mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: x : String
s : List String
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (s.length + [].length, s.length)
    ([].length + (x :: s).length, [].length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : (pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂)
    ((List.drop 1 (s' ++ [pre]) ++ l).length + [].length, (List.drop 1 (s' ++ [pre]) ++ l).length)
    ((pre :: l).length + s'.length, (pre :: l).length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + [].length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + (s' ++ [pre]).length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
all_goals grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
by
  by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b

Tactic:
simp [Function.extend_def, hb]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
rβ : β → β → Prop
f : α → β
dc : ∀ {a : α} {b : β}, rβ b (f a) → ∃ c, f c = b
a✝ : α
ha : Acc (InvImage rβ f) a✝
a : α
x✝ : β
h : rβ x✝ (f a)
a' : α
he : f a' = x✝
⊢ InvImage rβ f a' a

Tactic:
by simp_all [InvImage]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : 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✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
f₁ f₂ : α → α
⊢ e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

Tactic:
apply arrowCongr_comp

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑f = ⇑g.symm ↔ f = g.symm

Tactic:
Equiv.coe_inj

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f = g.symm
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ h, x.getLeft h = a

Tactic:
cases x <;> simp

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ h, x.getRight h = b

Tactic:
cases x <;> simp

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

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ g • a * g⁻¹ • a⁻¹ = 1

Tactic:
by rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ Option.elim' (f none) (f ∘ some) o = f o

Tactic:
cases o <;> rfl

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ BiTotal R ↔ IsEmpty α

Tactic:
simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
o : Option α
⊢ o.getD default = o.iget

Tactic:
cases o <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ o.casesOn' (f none) (f ∘ fun a ↦ some a) = f o

Tactic:
cases o <;> rfl

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ b, b < a

Tactic:
exact ⟨_, update_lt_self_iff.2 hb⟩

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ ((x : α) → (fun x ↦ β) x) = (α → β')

Tactic:
funext h'

Goal state after:
case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ ((x : α) → (fun x ↦ β') x) = (α → β')
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case isTrue
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : p
⊢ a h✝ ≠ ⊤

Tactic:
solve_by_elim

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

Goal state before:
pp: case isFalse
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : ¬p
⊢ b h✝ ≠ ⊤

Tactic:
solve_by_elim

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
M : α
⊢ ¬P M

Tactic:
induction M using WellFoundedGT.induction with
  | ind x IH =>
    by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊆ {x} ∧ s ≠ {x} ↔ s = ∅

Tactic:
subset_singleton_iff_eq,

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ (s = ∅ ∨ s = {x}) ∧ s ≠ {x} ↔ s = ∅
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ (fun x1 x2 ↦ x1 ⊓ x2) = minDefault

Tactic:
ext x y
  unfold minDefault
  split_ifs with h'
  exacts [inf_of_le_left h', inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h']

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

Goal state before:
pp: α : Type u
s : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False

Tactic:
H x hx,

Goal state after:
α : Type u
s : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ y
⊢ False
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]

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
← sup_sdiff_right_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ b \ c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ sᶜ ⊆ tᶜ

Tactic:
gcongr

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: α : Type u_1
s₁ s₂ t : Set α
h : s₁ ⊆ s₂
⊢ s₁ \ t ⊆ s₂ \ t

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
s t u : Set α
h : t ⊆ u
⊢ s \ u ⊆ s \ t

Tactic:
gcongr

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
o : Option α
⊢ (fun s ↦ Sum.elim some (fun x ↦ none) s) ((fun o ↦ o.elim (inr PUnit.unit) inl) o) = o

Tactic:
cases o <;> rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

Tactic:
· rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
    · exact ha.symm
    · exact ha.symm

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
exact
    le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

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

Goal state before:
pp: case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
refine ⟨?_, fun h => ⟨i, h, hi⟩⟩

Goal state after:
case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s → i ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁

Tactic:
rw [prod_subset_prod_iff, or_iff_left]
  rw [← Set.prod_eq_empty_iff]
  exact h.ne_empty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = univ ↔ range f ⊆ s

Tactic:
rw [← univ_subset_iff, ← image_subset_iff, image_univ]

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

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ range (toPullbackDiag f) = pullbackDiagonal f

Tactic:
rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)

Tactic:
simp only [eq_empty_iff_forall_notMem, mem_preimage] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ Disjoint s (range f)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₁ = s₂

Tactic:
← h.preimage_image_inter hs₁,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s = s₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
x : β
hx : x ∈ r
⊢ x ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝¹ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
a✝ : l < _n + 1
⊢ motive l

Tactic:
exact if hlm : l < m then lt l hlm else ge l (by lia) fun k _ ↦ ih k (by lia)

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

Goal state before:
pp: a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d

Tactic:
obtain ⟨k, rfl⟩ := hbc
  rw [Int.mul_ediv_cancel_left _ hb]
  rwa [Int.mul_assoc, Int.mul_eq_mul_left_iff hb] at h

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

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -(↑n + 1) = ofNat (m - n.succ)

Tactic:
ofNat_eq_natCast,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + 1) = ofNat (m - n.succ)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + 1) = ofNat (m - n.succ)

Tactic:
ofNat_eq_natCast,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + 1) = ↑(m - n.succ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ → t₁ = ∅ ∨ t₂.Nonempty

Tactic:
by_contra!; aesop

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ → t₁.Nonempty ∨ t₂ = ∅

Tactic:
by_contra!; aesop

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

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

Tactic:
conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
by rw [h, mul_inv_cancel_left]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = b * c⁻¹
⊢ a * c = b

Tactic:
by rw [h, inv_mul_cancel_right]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = b⁻¹ * c
⊢ b * a = c

Tactic:
by rw [h, mul_inv_cancel_left]

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

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

Tactic:
div_eq_iff_eq_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a = c * b ↔ a = b * c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
div_eq_iff_eq_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a = c / d * b ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff_mul_eq_mul]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
div_eq_iff_eq_mul,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a = c / d * b ↔ a / c = b / d
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
⊢ p a c → f a c = f a b * f b c

Tactic:
pac

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c

Tactic:
by
  have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
    intro b c rbc pab pbc pac
    obtain rab | rba := total_of r a b
    · exact hmul rab rbc pab pbc pac
    rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
    obtain rac | rca := total_of r a c
    · rw [hmul rba rac (symm pab) pac pbc]
    · rw [hmul rbc rca pbc (symm pac) (symm pab), mul_assoc, hf_swap (symm pac), mul_one]
  obtain rbc | rcb := total_of r b c
  · exact hmul' rbc pab pbc pac
  · rw [hmul' rcb pac (symm pbc) pab, mul_assoc, hf_swap (symm pbc), mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ (↑u)⁻¹ * ↑u = 1

Tactic:
← Units.val_inv_eq_inv_val,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u⁻¹ * ↑u = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * (↑u)⁻¹ = 1

Tactic:
← Units.val_inv_eq_inv_val,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * ↑u⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a = b * ↑c⁻¹
⊢ a * ↑c = b

Tactic:
by rw [h, inv_mul_cancel_right]

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
⊢ Surjective ⇑(map f)

Tactic:
rintro ⟨u, v, uv, vu⟩

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
u v : N
uv : u * v = 1
vu : v * u = 1
⊢ ∃ a, (map f) a = { val := u, inv := v, val_inv := uv, inv_val := vu }
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ ↑b * a = c

Tactic:
by rw [h, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ ↑u₁ * ↑u₂⁻¹ = 1

Tactic:
by rw [h, u₂.mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]

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✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ x✝⁻¹ * x✝ = 1

Tactic:
ext <;> exact inv_mul_cancel _

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ y = z

Tactic:
by
    dsimp only at h; rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑(match 0 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
simp [Nat.le_of_sub_eq_zero e]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
m n d₁ d₂ : α
hy : d₁ ∣ m
hz : d₂ ∣ n
⊢ d₁ * d₂ ∣ m * n

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
c : α
⊢ a * c ∣ b * c

Tactic:
gcongr

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n✝ : ℕ
a✝ : a ^ n✝ ∣ b ^ n✝
⊢ a ^ n✝ * a ∣ b ^ n✝ * b

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ a ^ n

Tactic:
gcongr

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

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ l.TFAE → (a :: l).TFAE

Tactic:
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)

Goal state after:
case head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

case head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
Module: Mathlib.Data.Int.Cast.Lemmas

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

Tactic:
ofNat_eq_natCast,

Goal state after:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑↑a✝ = 0
⊢ ofNat a✝ = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
← mul_add,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * (2 * b) + b) + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
← mul_add,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * (2 * b) + b + a) + 1 = 2 * (2 * a * b + b + a) + 1
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
⊢ a * a + a * b = 0

Tactic:
← mul_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
⊢ a * (a + b) = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * a + ↑u⁻¹ * a

Tactic:
← mul_add,

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * (a + a)
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a (min c b) = min (min a c) b

Tactic:
← min_assoc

Goal state after:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a c) b = min (min a c) b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b - c = a - c - b

Tactic:
rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]

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

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

Tactic:
by
  rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 1 + 0 ≤ 1 + 1

Tactic:
gcongr

Goal state after:
case bc
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1