Theorem: Usa2023P5.injective_of_permuted_rows (Compfiles/Usa2023P5.lean)

State before:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
⊢ Function.Injective2 fun r c => f r (p r c)
Tactic:
intro a1 a2 b1 b2 hab
State after:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
⊢ a1 = a2 ∧ b1 = b2

State before:
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
⊢ a1 = a2 ∧ b1 = b2
Tactic:
obtain ⟨ha1, hp1⟩ := hf hab
State after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a1 = a2
hp1 : p a1 b1 = p a2 b2
⊢ a1 = a2 ∧ b1 = b2

State before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a1 = a2
hp1 : p a1 b1 = p a2 b2
⊢ a1 = a2 ∧ b1 = b2
Tactic:
rw [ha1] at *
State after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b1 = b2

State before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b1 = b2
Tactic:
rw [hp a2 hp1]
State after:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b2 = b2

State before:
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b2 = b2
Tactic:
simp only [and_self]
State after:
no goals