mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b

Tactic:
simpa [I.eq_iff] using h

Goal state after:
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b

Tactic:
simpa [I.eq_iff] using h

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
← not_nontrivial_iff_subsingleton,

Goal state after:
α : Type u_1
⊢ ¬¬Nontrivial α ↔ Nontrivial α
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
← not_nontrivial_iff_subsingleton,

Goal state after:
α : Type u_3
⊢ ¬Nontrivial α ∨ Nontrivial α
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop
⊢ Decidable p

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
⊢ DecidablePred p

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → α → Prop
⊢ DecidableRel p

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α✝ : Sort u_1
α : Sort u_2
⊢ DecidableEq α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.IsEmpty.Defs

Goal state before:
pp: α : Sort u
β : Sort v
h : Nonempty α
inst✝ : IsEmpty β
⊢ IsEmpty (α → β)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f a₁ = f a₂
ne : ¬a₁ = a₂
⊢ c = c'

Tactic:
have ⟨f, hf⟩ := surj (if · = a₂ then c else c')

Goal state after:
α : Sort u_1
β : Sort u_2
f✝ : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f✝
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g ↦ g ∘ f✝) f = fun x ↦ if x = a₂ then c else c'
⊢ c = c'
Module: Mathlib.Data.Subtype

Goal state before:
pp: β : Sort u_2
γ : Sort u_3
p : β → Prop
g : { x // p x } → γ
j : β → γ
b : β
hb : ¬p b
⊢ extend val g j b = j b

Tactic:
by
  grind [Function.extend]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c

Tactic:
by
  induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → TransGen r a b → Prop
a : α
h : TransGen r a b
single : ∀ {a : α} (h : r a b), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
induction h with
  | single h => exact single h
  | @tail b c _ hbc h_ih =>
  apply h_ih
  · exact fun h ↦ head h (.single hbc) (single hbc)
  · exact fun hab hbc ↦ head hab _

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r d a

Tactic:
exact ⟨e, refl, ReflGen.single hde⟩

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid (α i)
⊢ Setoid ((i : ι) → α i)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ LeftInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
x✝ : Quot ra
a : α
⊢ Quot.map ⇑e.symm ⋯ (Quot.map ⇑e ⋯ (mk ra a)) = mk ra a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ RightInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
x✝ : Quot rb
a : β
⊢ Quot.map ⇑e ⋯ (Quot.map ⇑e.symm ⋯ (mk rb a)) = mk rb a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ m • n • a = n • m • a

Tactic:
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]

Goal state after:
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
⊢ f₁ (f₂ b) = b

Tactic:
inhabit δ
      exact congr_arg Prod.fst (h (b, default))

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {a b : α}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
simp [compare_eq_iff_eq]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ NoMinOrder α ↔ ∀ (x : α), ¬IsMin x

Tactic:
simp [noMinOrder_iff', IsMin, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ cmp x x = eq

Tactic:
cmp_eq_eq_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ x = x
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
M : α
hM : M > x
hM' : P M
⊢ False

Tactic:
exact IH _ hM hM'

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
let : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
⊢ Disjoint a b ↔ Disjoint ↑a ↑b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c

Tactic:
· rintro ⟨rfl, rfl⟩
    exact ⟨inf_idem _, sup_idem _⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
⊢ Preorder α

Tactic:
apply Function.Injective.preorder e

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c

Tactic:
exact sdiff_le_sdiff_right h

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c

Tactic:
exact sdiff_le_sdiff_right h

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s \ t = tᶜ ∩ s

Tactic:
rw [sdiff_eq, inter_comm]

Goal state after:
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rw [removeNone_some _ ⟨a, h⟩]

Goal state after:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ e (some x) = e none ↔ e.symm none = some x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
rintro (x | x) <;> simp

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
rintro (x | x) <;> simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)

Tactic:
exact fun _ => hnot_le_iff_codisjoint_right

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ≤ a ∆ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ Disjoint a b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ a ∈ t

Tactic:
rwa [hf ha _ hba.symm]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ b ∈ f ⁻¹' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
· simp [h, prod_eq_empty_iff.1 h]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁

Tactic:
rintro i ⟨his, hpi⟩
        simpa [*] using h i

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
rintro i ⟨his, hpi⟩
        simpa [*] using h i

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i

pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i) → ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i) → ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g ∘ f '' s

Tactic:
image_comp g f

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s

Tactic:
apply Subset.antisymm
  · rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
    exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩
  · rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩
    exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

Goal state after:
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
simp only [mul_left_comm, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a⁻¹ ^ 0 = (a ^ 0)⁻¹

Tactic:
by rw [pow_zero, pow_zero, inv_one]

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy (op (unop a)) (op (unop x)) (op (unop y))

Tactic:
semiconjBy_op

Goal state after:
α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy (unop a) (unop y) (unop x)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b

Tactic:
rw [← mul_div_assoc, mul_div_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: G : Type u_1
R : Type u_2
S : Type u_3
F : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
inst✝³ : FunLike F R S
inst✝² : MonoidHomClass F R S
inst✝¹ : FunLike G S R
inst✝ : MonoidHomClass G S R
f : F
g : G
hfg : LeftInverse ⇑g ⇑f
a : R
ha : IsUnit (f a)
⊢ IsUnit a

Tactic:
by rwa [isUnit_map_of_leftInverse g hfg] at ha

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
rw [Prod.mk_inj]

Goal state after:
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
rw [Prod.mk_inj]

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ ({ toFun := fun f ↦ f.extendDomain (Equiv.refl { x // p x }), map_one' := ⋯, map_mul' := ⋯ } (f.subtypePerm h₁)) x =
    f x

Tactic:
MonoidHom.coe_mk,

Goal state after:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ ({ toFun := fun f ↦ f.extendDomain (Equiv.refl { x // p x }), map_one' := ⋯ } (f.subtypePerm h₁)) x = f x
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 3 + 1 = 4

Tactic:
rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one,
    ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1 + 1) = 4
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddCommMonoid ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddMonoid ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ Monoid ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ CommSemigroup ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ Semigroup ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddGroup ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddCommSemigroup ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddSemigroup ℤ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
obtain hn | hn := natAbs_eq m <;> rw [hn]

Goal state after:
case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ ↑m.natAbs ∣ ↑n ↔ (↑m.natAbs).natAbs ∣ n

case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ -↑m.natAbs ∣ ↑n ↔ (-↑m.natAbs).natAbs ∣ n
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ AddCommMonoid ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ AddMonoid ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ Monoid ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ CommSemigroup ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ Semigroup ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ AddCommSemigroup ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Defs

Goal state before:
pp: ⊢ AddSemigroup ℕ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: z : ℤ
⊢ IsSquare z.sign ↔ 0 ≤ z

Tactic:
induction z using Int.induction_on with

Goal state after:
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
⊢ (fun x ↦ x * r) r' = (fun x ↦ x * r) 0

Tactic:
simp_rw [eq, zero_mul]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ (n + 1)

Tactic:
_root_.pow_succ',

Goal state after:
α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m * m ^ n) = ↑m ^ (n + 1)
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m * m ^ n) = ↑m ^ (n + 1)

Tactic:
_root_.pow_succ',

Goal state after:
α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m * m ^ n) = ↑m * ↑m ^ n
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x = 0

Tactic:
← mul_one x,

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f (x * 1) = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ x * z = y

Tactic:
by rw [h1, inverse_mul_cancel_right _ _ h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
⊢ IsUnit a

Tactic:
by
    cases subsingleton_or_nontrivial M₀
    · convert! h
    · contrapose h
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
by
  rw [div_eq_mul_inv]
  exact mul_ne_zero ha (inv_ne_zero hb)

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ 0 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
zero_add,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
zero_add,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ b ^ (2 * k + 3) = b ^ (2 * k + 1) * a ^ 2
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ b + a - (c + a) = b - c

Tactic:
add_tsub_add_eq_tsub_right

Goal state after:
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a b c : α
⊢ b - c = b - c