mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)

Tactic:
by rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + n) = a ^ (n + m)

Tactic:
Nat.add_comm

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (n + m) = a ^ (n + m)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
b : α
A : P → α
⊢ (dite P A fun x ↦ b) ≠ b ↔ ∃ h, A h ≠ b

Tactic:
by
  simp only [Ne, dite_eq_right_iff, not_forall]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f i ≍ Function.const α (f default) x✝¹

Tactic:
rw [Subsingleton.elim i default]

Goal state after:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
by
  unfold extend
  congr

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : IsTrans α r'
h : r ≤ r'
⊢ TransGen r ≤ r'

Tactic:
simpa [transGen_eq_self] using TransGen.mono h

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
ext; rfl

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n + m] a = f^[n] a

Tactic:
Nat.add_comm

Goal state after:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[n + m] a = f^[n] a ↔ f^[n + m] a = f^[n] a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝ : α ≃ β
⊢ (fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝) = x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • 1 * a = r₂ • 1 * a

Tactic:
hr

Goal state after:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₂ • 1 * a = r₂ • 1 * a
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:
by
      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 : α
⊢ compareOfLessAndEq a b = Ordering.eq ↔ a = b

Tactic:
compareOfLessAndEq_eq_eq le_refl not_le

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a = b ↔ a = b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ cmp a b = compare a b

Tactic:
by
  refine ((compare_iff ..).2 ?_).symm
  unfold cmp cmpUsing; split_ifs with h1 h2
  · exact h1
  · exact h2
  · exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

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

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn hnm fun {k} ↦ next)

Tactic:
by
  induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]

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

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
· have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'

Tactic:
apply lt_iff_lt_of_cmp_eq_cmp

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
intro h i x hf hg

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b

Tactic:
· rintro ⟨c, rfl : _ = _ ⊔ _⟩
    exact le_sup_left

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

Goal state before:
pp: α : Type u
s : Set α
⊢ Nontrivial ↑s ↔ s.Nontrivial

Tactic:
by
  simp [← nontrivial_univ_iff, Set.Nontrivial]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : Option α
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) a) = a

Tactic:
cases a with

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)

Tactic:
rw [sup_inf_left, inf_sup_left y]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ CoheytingAlgebra α

Tactic:
apply e.injective.coheytingAlgebra <;> intros

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
y✝ x✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
y✝ x✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := ⋯
top : Top α := ⋯
hnot : HNot α := ⋯
⊢ e ⊤ = ⊤

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := ⋯
top : Top α := ⋯
hnot : HNot α := ⋯
⊢ e ⊥ = ⊥

case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a✝ : α
⊢ e (￢a✝) = ￢e a✝

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
b✝ a✝ : α
⊢ e (b✝ \ a✝) = e b✝ \ e a✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inl ⟨x, hx⟩

Tactic:
rw [dif_pos]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

Tactic:
by_cases h : p x <;> simp [h]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b

Tactic:
rw [← symmDiff_of_le ha]
  exact ((symmDiff_right_involutive a).toPerm _).eq_symm_apply.symm.trans eq_comm

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'

Tactic:
intro r x hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
x : α
hx : x ∈ f ⁻¹' s
⊢ x ∈ f ⁻¹' s'
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'

Tactic:
intro r x hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : x ∈ range f ∩ s
⊢ x ∈ range f ∩ s'
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (s.domRestrict f) ↔ InjOn f s

Tactic:
injOn_iff_injective

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (s.domRestrict f) ↔ Injective (s.domRestrict f)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' range Sum.inl = ∅

Tactic:
rw [← image_univ, preimage_inr_image_inl]

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

Goal state before:
pp: ι : Type u_8
α : ι → Type u_9
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'

Tactic:
simp [compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
by
  apply Set.preimage_subset_preimage_iff
  rw [hf.range_eq]
  apply subset_univ

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

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

Tactic:
· rintro ⟨ht₁, ht₂⟩ i his
    by_cases p i <;> simp_all

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')

Goal state after:
case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (fun x ↦ (f₁ x.1, f₂ x.2)) x = (fun x ↦ (f₁ x.1, f₂ x.2)) y → x = y

Tactic:
by simp_rw [Prod.ext_iff]; exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

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

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

Tactic:
← op_unop x,

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Tactic:
rw [divp, division_def, Units.val_mul]

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

Goal state before:
pp: M : Type u
inst✝ : Monoid M
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ

Tactic:
ext; rfl

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
f g : G →* M
⊢ (f * g).toHomUnits = f.toHomUnits * g.toHomUnits

Tactic:
ext; rfl

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
ext <;> apply pow_left_injective hn

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ (fun a ↦ a ^ n) a.1 = (fun a ↦ a ^ n) b.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ (fun a ↦ a ^ n) a.2 = (fun a ↦ a ^ n) b.2
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
rw [Hfa, zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
rw [Hfa, zero]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
by
  cases n with
  | ofNat n => exact subtypePerm_pow _ _ _
  | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

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

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

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add]
  apply congrArg
  decide

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Tactic:
by simp [mul_inv_rev]

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0

Tactic:
rw [← h, Nat.cast_zero]

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(m + 1 + n) = ↑(n + m.succ)

Tactic:
Nat.add_comm

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(n + (m + 1)) = ↑(n + m.succ)
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + 1 + (n + 1)) = -↑(n + 1 + (m + 1))

Tactic:
Nat.add_comm

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(n + 1 + (m + 1)) = -↑(n + 1 + (m + 1))
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x

Tactic:
rw [← add_smul, h, one_smul]

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

Goal state before:
pp: α : Type u
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0

Tactic:
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

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

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f (n + 1) = ↑(n + 1)

Tactic:
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯

Tactic:
ext; rfl

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ ↑a✝ ≠ 0

Tactic:
by rw [zpow_natCast]; exact pow_ne_zero _

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
by
  rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑a✝ = 0
⊢ ofNat a✝ = 0

Tactic:
exact congr_arg _ (Nat.cast_eq_zero.1 h)

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc.e_a
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (↑x + 1) = g (↑x + 1)

Tactic:
exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a - 2) ↔ Odd a

Tactic:
← odd_add_two (a := a - 2),

Goal state after:
α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a - 2 + 2) ↔ Odd a
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
simp [inv_le_iff_one_le_mul']

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
hb : 0 ≤ b
⊢ a * a < b * b → a < b

Tactic:
by
  simp only [← sq]
  exact lt_of_pow_lt_pow_left₀ _ hb

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

Goal state before:
pp: α : Sort ?u.9
β : Type ?u.24
x✝ : α ≃ β
⊢ (fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝) = x✝

Tactic:
ext; rfl

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

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a = extend (⇑e₂₃ ∘ ⇑e₁₂) f (fun a ↦ default) a

Tactic:
rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s

Tactic:
by
  haveI := @Std.Asymm.irrefl β s _
  refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
  · apply Std.Trichotomous.trichotomous (r := r) a b
    · exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)
    · exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)
  · refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_
    exact (irrefl _ <| · ▸ h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : r ≃r s
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝) = x✝

Tactic:
ext; rfl

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
x✝ : α ≃o β
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨RelIso.toRelEmbedding f, ⋯⟩) x✝) = x✝

Tactic:
ext; rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ f (f.symm y)

Tactic:
f.le_iff_le

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ f.symm y
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ b / d ≤ max (c / d) (d / a)

Tactic:
exact le_max_of_le_left <| div_le_div_right' hcd _

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (c ⊔ (a ⊔ c))) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
sup_comm c (a ⊔ c),

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))

Tactic:
div_mul_div_comm

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))