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

Goal state before:
pp: a b : Prop
⊢ (a ↔ b) = (b ↔ a)

Tactic:
rw [@iff_comm a b]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
⊢ Injective fun g ↦ extend f g e'

Tactic:
by
  intro g₁ g₂ hg
  refine funext fun x ↦ ?_
  have H := congr_fun hg (f x)
  simp only [hf.extend_apply] at H
  exact H

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)

Tactic:
refine Acc.intro (f a) fun b hr ↦ ?_

Goal state after:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
⊢ Acc rβ b
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
by
  induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c

Tactic:
by
  induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
b a b✝ : α
h : r a b✝
motive : (a : α) → TransGen r a b✝ → Prop
single : ∀ {a : α} (h : r a b✝), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), motive c h → motive a ⋯
⊢ motive a ⋯

Tactic:
exact single h

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b✝ : α
h : r a b✝
⊢ motive ⋯

Tactic:
exact single h

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ : α
⊢ EqvGen r a✝ a✝

Tactic:
exact .refl _

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

Goal state before:
pp: case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
x✝ : Quot ra
a : α
⊢ Quot.map ⇑e.symm ⋯ (Quot.map ⇑e ⋯ (mk ra a)) = mk ra a

Tactic:
simp only [Quot.map, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : Type u_9
inst✝ : One M
i : ι
x : M
j : ι
⊢ mulSingle i x j = mulSingle j x i

Tactic:
simp [mulSingle_apply, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
classical
  funext x
  simp [Function.extend_def, apply_dite Inv.inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ min a a = a

Tactic:
min_def,

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

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

Tactic:
min_def,

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

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x < update x i a ↔ x i < a

Tactic:
by simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: 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)

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

Goal state after:
case ind.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)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
by
  rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

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 ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
inf_sup_right,

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') ⊔ x' ⊓ (y ⊓ y') = ⊥
Module: Mathlib.Order.Lattice

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

Tactic:
simp only [sup_inf_left, sup_comm _ c]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : 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
a b : α
⊢ a ≤ a ⊔ b

Tactic:
rw [← le, map_sup]
    exact le_sup_left

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c

Tactic:
himp_himp,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ⇨ c = b ⊓ a ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ b ⇨ a = b ⇨ a

Tactic:
himp_himp,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⊓ b ⇨ a = b ⇨ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d

Tactic:
by simp_rw [sdiff_le_iff, sup_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ a ⇨ ⊥ = a ⇨ ⊥

Tactic:
himp_himp,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⊓ a ⇨ ⊥ = a ⇨ ⊥
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : e (some x) = e none
hn : e none = none
⊢ False

Tactic:
exact Option.some_ne_none _ (e.injective h)

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

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

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ (y ⊔ z) ⊓ (x ⊔ z) = y

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ (x ⊔ z) ⊔ z ⊓ (x ⊔ z) = y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊔ y \ z ⊓ y = x ⊓ y ⊔ y \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (y ⊔ z) ⊔ x ⊓ (y ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z ⊓ (z ⊔ x)) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b

Tactic:
symmDiff_sup_inf

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b = a ⊔ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ

Tactic:
inf_sup_right,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Module: Mathlib.Data.Set.Prod

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

Tactic:
have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩

Tactic:
· obtain ⟨a, ha, rfl⟩ := h' hb
    exact ⟨⟨a, ha⟩, rfl⟩

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
intro h x a

Goal state after:
case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : ↑s
a : x ∈ val ⁻¹' t
⊢ x ∈ val ⁻¹' u
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f g : OneHom M N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
ι : 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
F : Type u_9
inst✝¹ : One M
inst✝ : One N
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
f g : M →ₙ* N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
ι : 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
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : 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
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
f g : M →* N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
ι : 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
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
g : M →* N
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h : (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = (fun f ↦ f.toFun) g
⊢ { toOneHom := toOneHom✝, map_mul' := map_mul'✝ } = g
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
f g : M ≃* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
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
g : M ≃* N
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
h₁ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.toFun = g.toFun
h₂ : { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }.invFun = g.invFun
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
⊢ BijOn g (p₁ '' s) (p₂ '' t)

Tactic:
by
  obtain ⟨h1, h2, h3⟩ := hbij
  refine ⟨?_, hinj, ?_⟩
  · rintro _ ⟨a, ha, rfl⟩
    exact ⟨f a, h1 ha, by rw [comm a]⟩
  · rintro _ ⟨b, hb, rfl⟩
    obtain ⟨a, ha, rfl⟩ := h3 hb
    grind

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1

Tactic:
rw [zero, one]

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
Module: Mathlib.Data.Nat.Cast.Defs

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

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

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

Goal state before:
pp: case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ 1 • (x⁻¹ * x) = 1

Tactic:
inv_mul_cancel₀ hx,

Goal state after:
case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ 1 • 1 = 1
Module: Mathlib.Algebra.CharZero.Defs

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

Tactic:
H n

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

case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h : (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun f ↦ f.toFun) g
⊢ { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f g : α →+* β
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
g : α →+* β
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹

Tactic:
simp [h.resolve_right ha]

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

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

Tactic:
cast_zero

Goal state after:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : n = 0
⊢ 0 = 0
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✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ -1 • a + a = 0

Tactic:
nth_rw 2 [← one_smul R a]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ -1 • a + 1 • a = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : NonAssocSemiring α
x : α
⊢ (x ∈ Set.range fun x ↦ 2 * x) ↔ x ∈ {a | Even a}

Tactic:
simp [eq_comm, two_mul, Even]

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ^ (n + 1) ≤ 1

Tactic:
by rw [zero_pow n.succ_ne_zero]; exact zero_le_one

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a < c * b

Tactic:
refine (add_lt_add_iff_right (d * b + d * a)).1 ?_

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) < c * b + (d * b + d * a)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
α : Sort u
β : Sort v
g : α ↪ β
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝, inj' := inj'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, inj' := inj'✝ } = g
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (-↑(n + 1))

Tactic:
rw [zpow_neg, inv_nonneg, zpow_natCast]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ 1 < a ^ n ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

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₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ a ^ n < 1 ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right₀ ha]

Goal state after:
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 : G₀
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff₀ hb, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r →r s
h : (fun o ↦ o.toFun) f = (fun o ↦ o.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r →r s
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h : (fun o ↦ o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ } = (fun o ↦ o.toFun) g
⊢ { toFun := toFun✝, map_rel' := map_rel'✝ } = g
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₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c < b / a

Tactic:
lt_div_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c * a < b
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 β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f g : α →o β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : α →o β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝, monotone' := monotone'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, monotone' := monotone'✝ } = g
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1

Tactic:
rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
    inf_assoc, inf_of_le_left ha]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ

Tactic:
apply le_of_mul_le_of_one_le_left _ (one_le_mabs _)

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |?m.37|ₘ ≤ |a / b|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℤ
hc : x.gcd y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! hc

Goal state after:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℤ
hc : x.gcd y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! hc
  rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

Goal state after: