request for help

Stream: mathlib4

[Arien Malec]

Could I ask someone to look at map_inv₀ in mathlib4#920?

if I get it to:

@[simp]
theorem map_inv₀ : f a⁻¹ = (f a)⁻¹ := by
  by_cases h : a = 0 <;>
  apply eq_inv_of_mul_eq_one_left <;>
  rw [← map_mul, inv_mul_cancel, map_one]
  . contradiction
  . assumption

I get the very confusing error:

tactic 'contradiction' failed
case pos.h
f: F
ab: G₀
h: a = 0
⊢ a ≠ 0

so I'm probably missing something super basic.

[Kevin Buzzard]

The contradiction tactic is not expected to prove that goal. The contradiction tactic proves an arbitrary goal if there are two contradictory hypotheses. Is that what's confusing you?

[Ruben Van de Velde]

You got misdirected at some point - this works:

/-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
@[simp]
theorem map_inv₀ : f a⁻¹ = (f a)⁻¹ := by
  by_cases h : a = 0
  · simp [h, map_zero f]
  · apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel h, map_one]
#align map_inv₀ map_inv₀

[Ruben Van de Velde]

(I pushed that)

[Arien Malec]

I was both confused by contradiction and by how I got into that state.

[Arien Malec]

So generally confused...

[Ruben Van de Velde]

In the a = 0 case, apply eq_inv_of_mul_eq_one_left gives you an unprovable goal