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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsLeftRegular a
eq : a * b = 1
⊢ (fun x ↦ a * x) (b * a) = (fun x ↦ a * x) 1

Tactic:
simp [← mul_assoc, eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a * a

Tactic:
rw [zpow_ofNat, pow_two]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
· exact ⟨x₂, h⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
⊢ Nontrivial β

Tactic:
obtain ⟨f, g, h⟩ := exists_pair_ne (α → β)

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : f ≠ g
⊢ Nontrivial β
Module: Mathlib.Logic.Basic

Goal state before:
pp: α₁ α₂ : Sort u
β₁ : α₁ → Sort v
β₂ : α₂ → Sort v
f₁ : (a : α₁) → β₁ a
f₂ : (a : α₂) → β₂ a
a₁ : α₁
a₂ : α₂
hargs : a₁ ≍ a₂
ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₂

Tactic:
cases hargs

Goal state after:
case refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
β₂ : α₁ → Sort v
f₂ : (a : α₁) → β₂ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Subsingleton ι
P : ι → ι → Prop
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i

Tactic:
refine forall_congr' fun i ↦ ?_
  have : Nonempty ι := ⟨i⟩
  simp [Subsingleton.elim _ i]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
cases h with

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : Std.Refl r'
h : r ≤ r'
⊢ ReflGen r ≤ r'

Tactic:
by
  simpa [reflGen_eq_self] using ReflGen.mono h

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

Tactic:
cases h with

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (fun x2 ↦ ((m • n) • p) • x2) = fun x2 ↦ (m • n • p) • x2

Tactic:
smul_assoc

Goal state after:
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 M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (MulOpposite.unop m • n) • a = MulOpposite.unop m • n • a

Tactic:
smul_assoc

Goal state after:
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 M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = MulOpposite.unop m • n • 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 N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • MulOpposite.unop n • a

Tactic:
← unop_smul_eq_smul (m • n) a,

Goal state after:
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 N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ MulOpposite.unop (m • n) • a = m • MulOpposite.unop n • 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 N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • MulOpposite.unop n) • a = m • MulOpposite.unop n • a

Tactic:
smul_assoc

Goal state after:
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 N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • MulOpposite.unop n • a = m • MulOpposite.unop n • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ r • s • x = s • r • x

Tactic:
rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ y * x • 1 = x • y

Tactic:
rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
p : P
q : Q
m : M
⊢ (m • p) • q = m • p • q

Tactic:
smul_assoc

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
induction a using WellFoundedLT.induction generalizing a' b with

Goal state after:
case ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
  by_cases P <;> by_cases Q <;> simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAnti (f ∘ ⇑ofDual) ↔ StrictMono f

Tactic:
strictAnti_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono f ↔ StrictMono f
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
| succ m ih =>

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

Tactic:
rw [← Nat.add_le_add_iff_right] at hle

Goal state after:
case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle✝ : x ≤ y
hle : x + ?m.52 ≤ y + ?m.52
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ ℕ
Module: Mathlib.Data.Set.Disjoint

Goal state before:
pp: α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s

Tactic:
rw [disjoint_comm, disjoint_left]

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

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
by
  simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]

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

Goal state before:
pp: f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
hc : ∀ (n : ℕ), f n ≤ c
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
by
  induction c with
  | zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
  | succ c ih =>
    by_cases! h : ∀ n, f n ≤ c
    · exact ih h
    · obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; lia
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; lia

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (a : β) (b : α), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a

Tactic:
rw [forall_comm]; simp only [Iff.comm]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
⊢ SemilatticeInf α

Tactic:
by
  let min := e.min
  let partialOrder := e.partialOrder
  apply e.injective.semilatticeInf <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ b \ c ≤ a \ c

Tactic:
by simpa [sup_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a < aᶜ ↔ a = ⊥

Tactic:
rw [lt_iff_le_and_ne]

Goal state after:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ x ⇨ y = y ⊔ xᶜ

Tactic:
ext <;> simp [himp_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)

Tactic:
symmDiff_symmDiff_left,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a ∆ (b ∆ c)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ (piCongrLeft' (fun x ↦ P) e).symm = piCongrLeft' (fun a ↦ P) e.symm

Tactic:
by ext; simp [piCongrLeft']

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

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
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
⊢ LeftInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

Tactic:
rintro ⟨_ | _, _⟩ <;> rfl

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

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
α : Type ?u.13
⊢ LeftInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
rintro ⟨_ | _, _⟩ <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Tactic:
apply inf_left_right_swap

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := hs

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (f '' s).Nontrivial
Module: Mathlib.Data.Set.Prod

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

Tactic:
by
  ext f
  refine ⟨fun h => ?_, ?_⟩
  · constructor <;>
      · rintro i ⟨his, hpi⟩
        simpa [*] using h i
  · rintro ⟨ht₁, ht₂⟩ i his
    by_cases p i <;> simp_all

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
⊢ range (Pi.map f) = univ.pi fun i ↦ range (f i)

Tactic:
by
  simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [Set.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, range f = graphOn (⇑e) univ
Module: Mathlib.Data.Set.Function

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

Tactic:
rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [← mul_div_assoc, div_mul_cancel]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b * c⁻¹ ↔ a * c = b

Tactic:
h.eq_mul_inv_iff_mul_eq

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c = b ↔ a * c = b
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : 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✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)

Tactic:
simpa using Equiv.congr_fun h i

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

Goal state before:
pp: case right
α : 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✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)

Tactic:
simpa using Equiv.congr_fun h i

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ 0 • m = 0

Tactic:
change (f 0) • m = 0

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ f 0 • m = 0
Module: Mathlib.Algebra.CharZero.Defs

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

Tactic:
| succ m ih =>

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

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

Tactic:
by
  unfold subNatNat
  cases e : n - m
  · simp [Nat.le_of_sub_eq_zero e]
  · rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

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

Goal state before:
pp: case inl.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n
⊢ ∀ (n : ℤ), ↑(↑(m + 1) * n) = ↑↑(m + 1) * ↑n

Tactic:
| succ m ih =>

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

Goal state before:
pp: case inr.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n
⊢ ∀ (n : ℤ), ↑(-↑(m + 1) * n) = ↑(-↑(m + 1)) * ↑n

Tactic:
| succ m ih =>

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

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

Tactic:
obtain hn | hn := natAbs_eq n <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.dvd_neg]

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

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

Tactic:
convert! h

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u

Tactic:
simp only [divp, sub_mul, sub_right_inj]
  rw [mul_assoc, Units.mul_inv, mul_one]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
by simp only [Int.cast_smul_eq_zsmul, map_zsmul]

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
by
  rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a * c ≤ b * d

Tactic:
by grw [h₁, h₂]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ b ≤ c / a ↔ a * b ≤ c

Tactic:
rw [le_div_iff_mul_le, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ a * c = a * b ↔ c = b

Tactic:
by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_right (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_right (h.lt_of_ne h') a |>.ne

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * b⁻¹ ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
mul_inv_le_inv_mul_iff

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c ≤ b / c ↔ a ≤ b

Tactic:
div_le_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c * c ↔ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a / c ≤ b / c ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hc, div_mul_cancel₀ _ hc.ne']

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a / b ≤ c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [inv_nonneg.2 <| hd.le.trans hdb, hc, hd]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ (a + b) ^ 2 ≤ (a + b) * (a + b)

Tactic:
sq

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ (a + b) * (a + b) ≤ (a + b) * (a + b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
rw [le_div_iff₀ hc, mul_comm]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
div_le_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b ≤ a * c ↔ b ≤ c * a
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✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ f (g x✝) = x✝

Tactic:
rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (a * a) = b ^ n * a ^ 2

Tactic:
sq

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (a * a) = b ^ n * (a * a)
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs ≤ ↑a.natAbs ^ 2

Tactic:
sq

Goal state after:
a : ℤ
⊢ ↑a.natAbs ≤ ↑a.natAbs * ↑a.natAbs