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

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

Tactic:
by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

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

Goal state before:
pp: α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y

Tactic:
exact Subsingleton.elim

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
rw [← not_exists]

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
by_cases h : p

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : ¬p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
by_cases h : p

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : ¬p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b

Tactic:
simpa using h.smul_left r⁻¹

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ a ≤ b

Tactic:
rw [hab]

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

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
exact compare_lt_iff_lt

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ min a b = if a < b then a else b

Tactic:
min_comm,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ min b a = if a < b then a else b
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤

Tactic:
by
      rw [map_top]
      exact le_top _

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

Tactic:
by
  rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ ⊥ ⊔ x' ⊓ (y ⊓ y') = ⊥

Tactic:
bot_sup_eq,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x' ⊓ (y ⊓ y') = ⊥
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ {a} ∩ s = {a}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
rw [← H, @sup_le_iff α A, H, H]

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
h1 : e.symm (e (some x)) = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
rw [symm_apply_apply] at h1

Goal state after:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ ¬a ∈ {b}

Tactic:
by simpa

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ BiheytingAlgebra α

Tactic:
apply e.injective.biheytingAlgebra

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_compl
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
calc
      x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by
          rw [sup_inf_right]
      _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
          rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x := by simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ BiheytingAlgebra α

Tactic:
apply e.injective.biheytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

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
α : Type ?u.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ LeftInverse (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) fun b ↦ ⟨inr b.fst, b.snd⟩) fun x ↦
    match x with
    | ⟨inl x, y⟩ => inl ⟨x, y⟩
    | ⟨inr x, y⟩ => inr ⟨x, y⟩

Tactic:
rintro ⟨x|x,y⟩

Goal state after:
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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inl x, y⟩) =
    ⟨inl x, y⟩

case inr
α✝ : 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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inr x, y⟩) =
    ⟨inr x, y⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = ⊥ ⊔ (a ⊓ b) \ c

Tactic:
bot_sup_eq,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ c
Module: Mathlib.Order.SymmDiff

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

Tactic:
by simp_rw [symmDiff_assoc, symmDiff_comm]

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

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ s

Tactic:
← yvaleq

Goal state after:
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
by
  classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

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 : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', range f = graphOn f' univ

Tactic:
by
  refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
  ext x
  simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]
  refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
  rintro ⟨g, rfl⟩
  exact hf _ _ (hf₁ (f g).1).choose_spec

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
⊢ Surjective (Prod.fst ∘ ⇑(Equiv.prodComm β γ) ∘ f)

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b

Tactic:
simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)

Tactic:
mul_inv_rev,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a * a ^ (n + 1))⁻¹ * a

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹ * a⁻¹ * a
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n) * a⁻¹

Tactic:
← ihn,

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + -↑n) * a⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a 1 n

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ x ^ ↑n = 1

Tactic:
by simpa

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
⊢ IsUnit a → IsUnit (a ^ n)

Tactic:
by
  rintro ⟨u, rfl⟩; exact ⟨u ^ n, rfl⟩

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : Group M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ (f x)⁻¹ * f x = 1

Tactic:
by rw [← inv, ← mul, inv_mul_cancel, one]

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

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

Tactic:
mul_inv_rev,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b * (b⁻¹ * a⁻¹) = a⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ (n + 1) • a = n • a + a

Tactic:
by change (n + 1) • a = n • a + a; rw [add_nsmul, one_nsmul]

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
u v : M
uv : f u * f v = 1
vu : f v * f u = 1
⊢ f (u * v) = f 1

Tactic:
by simpa

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
u v : M
uv : f u * f v = 1
vu : f v * f u = 1
⊢ f (v * u) = f 1

Tactic:
by simpa

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:
rwa [isUnit_map_of_leftInverse g hfg] at ha

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : M
⊢ a * a = 1

Tactic:
subsingleton

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
x✝ : Mˣ
⊢ ↑x✝ = 1

Tactic:
subsingleton

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✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f a * f b = 0

Tactic:
rw [← mul, H, zero]

Goal state after:
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✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor <;> ext i <;> simpa using Equiv.congr_fun h i

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False

Tactic:
rw [ha, div_zero] at h

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a * a ^ (n + 1))⁻¹ * a

Tactic:
mul_inv_rev,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * a⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n) * a⁻¹

Tactic:
← ihn,

Goal state after:
case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + -↑n) * a⁻¹
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case refine_3
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_sub_one hkm, ih']

Goal state after:
case refine_3
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ ∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ (n + 1) • a = ↑(n + 1) * a

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
have := IH ⟨bc, ch⟩ (ab ∘ h_last)

Goal state after:
case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
A : Type u_6
inst✝² : AddMonoidWithOne A
inst✝¹ : FunLike F A B
inst✝ : AddMonoidHomClass F A B
f : F
h : f 1 = 1
⊢ ((↑f).comp (Nat.castAddMonoidHom A)) 1 = 1

Tactic:
by simpa

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

Goal state before:
pp: A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : f 1 = 1
⊢ f 1 = (castAddHom A) 1

Tactic:
by simp [h1]

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : AddGroupWithOne α
inst✝² : AddGroupWithOne β
inst✝¹ : FunLike F α β
inst✝ : AddMonoidHomClass F α β
f : F
h₁ : f 1 = 1
⊢ ((↑f).comp (castAddHom α)) 1 = 1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a / c < b / c ↔ a < b

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
ha : 0 ≤ a
h : a < a * b
⊢ a * 1 < a * b

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
hb : 0 ≤ b
h : b < a * b
⊢ 1 * b < a * b

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
ha : 0 < a
h : a ≤ a * b
⊢ a * 1 ≤ a * b

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
hb : 0 < b
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
by simpa

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Tactic:
by
  rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)] <;>
    apply mul_self_nonneg

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
by
  rw [← denselyOrdered_orderDual]
  let e : Xᵒᵈ ≃o Y := ⟨OrderDual.ofDual.trans (f : X ≃ Y), ?_⟩
  · exact denselyOrdered_iff_of_orderIsoClass e
  · simp only [Equiv.trans_apply, EquivLike.coe_coe, OrderDual.forall, OrderDual.ofDual_toDual,
      OrderDual.toDual_le_toDual]
    intro a b
    rw [hf.le_iff_ge]

Goal state after: