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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (SymmGen r) = EqvGen r

Tactic:
by
  rw [← eqvGen_eq_reflTransGen, eqvGen_symmGen]

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

Goal state before:
pp: α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ e.permCongr (Equiv.refl α') = Equiv.refl β'

Tactic:
by
  simp [permCongr_def]

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

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

Tactic:
exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

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

Goal state before:
pp: case h
M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : α
X✝ : M
⊢ MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a

Tactic:
exact (IsCentralScalar.op_smul_eq_smul _ a).symm

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

Goal state before:
pp: α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
max_def,

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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h₂

Goal state after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b

Tactic:
by
  rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t

Tactic:
inter_nonempty

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t

Tactic:
by
  simp_rw [inter_nonempty]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right]

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

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ e.symm none = some x

Tactic:
exact (e.eq_symm_apply.mpr h2).symm

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z

Tactic:
exact sdiff_le_sdiff_right h.1

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y

Tactic:
← sup_sdiff_cancel_right hx

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| x ⊔ y \ x
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

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.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 α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.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 α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.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 α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.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 α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

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

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.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 α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sdiff_sdiff_left, sdiff_sup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (preimage f ∘ ofPred) ↔ Injective f

Tactic:
← Surjective.of_comp_iff' Set.mem_bijective

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (Membership.mem ∘ preimage f ∘ ofPred) ↔ Injective f
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
γ : Type u_3
δ : Type u_4
s : Set α
a b : α → γ × δ
⊢ EqOn a b s ↔ EqOn (Prod.fst ∘ a) (Prod.fst ∘ b) s ∧ EqOn (Prod.snd ∘ a) (Prod.snd ∘ b) s

Tactic:
by
  grind [EqOn]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)

Tactic:
rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩)

Goal state after:
case mpr.inl
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (s.piecewise f g)

case mpr.inr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (s.piecewise f g)
Module: Mathlib.Data.Set.Image

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

Tactic:
preimage_inl_image_inr

Goal state after:
α : Type u_1
β : Type u_2
⊢ ∅ = ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
hf : EqOn f f' s
hg : EqOn g g' t
⊢ EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)

Tactic:
by
  grind [EqOn]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
⊢ Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i

Tactic:
by
  refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_
  have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
    if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
  choose a hab hat using this
  exact ⟨a, hat, funext hab⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]
  simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
inst✝³ : EquivLike F α β
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
h1 : M ≃* N
h2 : N ≃* P
x y : M
⊢ h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y)

Tactic:
rw [map_mul, map_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ a = b

Tactic:
← one_div_one_div a,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ 1 / (1 / a) = b
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by
  rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
subst v'

Goal state after:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v, inv := i₂, val_inv := vi₂, inv_val := iv₂ }
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
by simp only [HPow.hPow, Pow.pow]; ext; simp [pow_succ]

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

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

Tactic:
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

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

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ n) ∘ c f = (c f)^[n] ∘ c f

Tactic:
hom_coe_pow c h1 hmul f n

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ (c f)^[n] ∘ c f = (c f)^[n] ∘ c f
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).1 = (x✝² * (x✝¹ * x✝)).1

Tactic:
exact mul_assoc ..

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

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).2 = (x✝² * (x✝¹ * x✝)).2

Tactic:
exact mul_assoc ..

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ a * b = 0

Tactic:
rw [ha, zero_mul]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
by
    by_cases hx : p x
    · exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx
    · rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
      exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a = 0

Tactic:
by
  rw [← mul_one a, ← h, mul_zero]

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

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

Tactic:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • -x + r • x = 0

Tactic:
← smul_add,

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • (-x + x) = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]

Goal state after:
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_assoc,

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

Goal state before:
pp: M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m

Tactic:
rw [← add_smul, add_sub_cancel, one_smul]

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.refine
     "refine"
     (Term.anonymousCtor
      "⟨"
      [(Term.fun "fun" (Term.basicFun [`t] [] "↦" (Term.syntheticHole "?" "_")))
       ","
       (Term.fun
        "fun"
        (Term.basicFun
         [`h]
         []
         "↦"
         (Term.app
          `h.elim
          [(Term.paren
            (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
            (Term.fun "fun" (Term.basicFun [(Term.hole "_")] [] "↦" `inferInstance))
            ")")
           (Term.paren
            (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
            (Term.fun "fun" (Term.basicFun [(Term.hole "_")] [] "↦" `inferInstance))
            ")")])))]
      "⟩"))
    []
    (Tactic.rwSeq
     "rw"
     (Tactic.optConfig [])
     (Tactic.rwRuleSeq
      "["
      [(Tactic.rwRule [] `or_iff_not_imp_right) "," (Tactic.rwRule [] `not_subsingleton_iff_nontrivial)]
      "]")
     [])
    []
    (Tactic.exact
     "exact"
     (Term.fun
      "fun"
      (Term.basicFun
       [(Term.hole "_")]
       []
       "↦"
       (choice
        («term{}» "{" "}")
        (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))])))

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹

Tactic:
Units.inv_mul_cancel_left

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = a * ↑x⁻¹
Module: Mathlib.Algebra.Group.Semiconj.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (↑a * x) * ↑a⁻¹ = x * ↑a⁻¹

Tactic:
Units.inv_mul_cancel_left

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ x * ↑a⁻¹ = x * ↑a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
by_cases hab : IsUnit (a * b)

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  exact h.mul_right h'.inv_right₀

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ (a ^ k)⁻¹ʳ * b = c ↔ b = a ^ k * c

Tactic:
Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ b = a ^ k * c ↔ b = a ^ k * c
Module: Mathlib.Algebra.Ring.Units

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

Tactic:
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

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

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a = 1 ∨ a = -1

Tactic:
← (Commute.one_right a).mul_self_eq_mul_self_iff,

Goal state after:
R : Type u
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a * a = 1 * 1
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]

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

Goal state before:
pp: case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ b * (k + k) = b * k + b * k

Tactic:
rw [mul_add]

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

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

Tactic:
Units.inv_mul_cancel_left

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = a
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
by
  grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLT α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le; exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩

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 d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Tactic:
by
  rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ a < b * c

Tactic:
← inv_mul_lt_iff_lt_mul,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ b⁻¹ * a < c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

pp: case refine_2
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
· exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)

Goal state after:
case refine_2
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
⊢ 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

Tactic:
rintro (⟨ha, hb⟩ | ⟨ha, hb⟩)

Goal state after:
case inl
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

case inr
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ x * a) x✝¹ = (fun x ↦ x * a) x✝
⊢ x✝¹ = x✝

Tactic:
by
    obtain ha | ha := ha.lt_or_gt
    exacts [(strictAnti_mul_right ha).injective h, (strictMono_mul_right_of_pos ha).injective h]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
⊢ Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

Tactic:
intro h x h₁ h₂

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : x ≤ a₁
h₂ : x ≤ a₂
⊢ x ≤ ⊥