Theorem: Fintype.invFun_eq_invFun (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (invFun f) x = (invFun f') y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
simp [invFun]
State after:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a

State before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
constructor
State after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y → ∃ a, ↑x = f a ∧ ↑y = f' a

case mpr
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (∃ a, ↑x = f a ∧ ↑y = f' a) → f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y

State before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y → ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
intro h
State after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ∃ a, ↑x = f a ∧ ↑y = f' a

State before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
refine ⟨_, ?_, h.symm⟩
State after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ↑x = f ↑((Finset.mapEquiv Finset.univ f).symm x)

State before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ↑x = f ↑((Finset.mapEquiv Finset.univ f).symm x)
Tactic:
simp [Finset.app_mapEquiv_symm]
State after:
no goals

State before:
case mpr
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (∃ a, ↑x = f a ∧ ↑y = f' a) → f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Tactic:
rintro ⟨a,h,h'⟩
State after:
case mpr.intro.intro
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
a : α
h : ↑x = f a
h' : ↑y = f' a
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y

State before:
case mpr.intro.intro
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
a : α
h : ↑x = f a
h' : ↑y = f' a
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Tactic:
simp_all
State after:
no goals