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

Goal state before:
pp: α : Sort u_1
r p q : α → Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x

Tactic:
by
  simp only [exists_prop]
  exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)

Tactic:
induction ha with | intro a _ ih => ?_

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)
⊢ Acc rβ (f a)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
⊢ Relation.Map (r on f) f f = r

Tactic:
by
  ext x y
  have _ := hsurj x
  have _ := hsurj y
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
by
  use cases_head
  rintro (rfl | ⟨c, hac, hcb⟩)
  · rfl
  · exact head hac hcb

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
by
  rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]

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

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

Tactic:
min_assoc

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min b (min a c) = min b (min a c)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)

Tactic:
rw [leRec_succ]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ (f ∘ rangeSplitting f) x✝ = ↑x✝

Tactic:
simp only [Function.comp_apply]

Goal state after:
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ f (rangeSplitting f x✝) = ↑x✝
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c

Tactic:
rwa [inf_comm]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

pp: case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b

Tactic:
· intro h
    exact ⟨b, (sup_eq_right.mpr h).symm⟩

Goal state after:
case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x

Tactic:
simp only [sup_le_iff]

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
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 ⊔ y ≤ c

Tactic:
simp only [sup_le_iff]

Goal state after:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
⊢ p (max a b)

Tactic:
by rwa [sup_eq_right.2 h]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_right_comm

Goal state after:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
⊢ RightInverse (fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)

Tactic:
by
    rintro ⟨f, g⟩
    ext1 <;> grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i, i ∈ s ∧ Disjoint (t₁ i) (t₂ i)

Tactic:
by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty

Tactic:
by
  rw [← image_preimage_coe, image_nonempty]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update f i y j ∈ t j

Tactic:
obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
⊢ f '' s = g ⁻¹' s

Tactic:
ext x
  constructor
  · rintro ⟨y, hy, rfl⟩
    rw [mem_preimage, hgf hy]; exact hy
  · intro hx
    refine ⟨g x, hx, Set.InjOn.rightInvOn_of_leftInvOn ginj hgf (Set.mapsTo_preimage g s) ?_ hx⟩
    intro y hy
    simpa [hgf hy] using hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H✝ : Type u_6
F : Type u_7
inst✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
by
        { simp only [map_div]
          simp only [mul_inv_cancel, one_mul, inv_inv] }

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

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (fun x ↦ (f₁ x.1, f₂ x.2)) x = (fun x ↦ (f₁ x.1, f₂ x.2)) y → x = y

Tactic:
simp_rw [Prod.ext_iff]; exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ 1 * a ^ n = a * a ^ n

Tactic:
zpow_one

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a * a ^ n = a * a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a * a ^ n = a ^ 1 * a ^ n

Tactic:
zpow_one

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a * a ^ n = a * a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ 1 * g ^ ↑n)

Tactic:
zpow_one

Goal state after:
case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g * g ^ ↑n)
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₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x)⁻¹⁻¹ = f x

Tactic:
← inv,

Goal state after:
M₁ : Type u_1
M₂✝ : Type u_2
inst✝⁴ : Mul M₂✝
inst✝³ : One M₂✝
inst✝² : Pow M₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x⁻¹)⁻¹ = f x
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₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ (f x⁻¹)⁻¹ = f x

Tactic:
← inv,

Goal state after:
M₁ : Type u_1
M₂✝ : Type u_2
inst✝⁴ : Mul M₂✝
inst✝³ : One M₂✝
inst✝² : Pow M₂✝ ℕ
M₂ : Type u_3
inst✝¹ : Inv M₂
inst✝ : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x⁻¹⁻¹ = f x
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✝ : DivInvMonoid 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 y : M₁
⊢ f x / f y = f x * (f y)⁻¹

Tactic:
← inv,

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✝ : DivInvMonoid 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 y : M₁
⊢ f x / f y = f x * f y⁻¹
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:
← inv,

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✝ : 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
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a * a⁻¹ = 1

Tactic:
rintro ⟨u, rfl⟩
  rw [← Units.val_inv_eq_inv_val, Units.mul_inv]

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
⊢ c (f ^ 0) = (c f)^[0]

Tactic:
by
    rw [pow_zero, h1]
    rfl

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

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
simp [mul_right_inj', ha]

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:
ha,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ 0 * b = 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
⊢ (f 0)⁻¹ = f 0

Tactic:
← inv,

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
⊢ f 0⁻¹ = f 0
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap y z * swap x y * swap y z = swap z x

Tactic:
by
  nth_rewrite 3 [← swap_inv]
  rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
x : G₀
hx : f x ≠ 0
⊢ f x * (f x)⁻¹ = 1

Tactic:
← inv,

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
x : G₀
hx : f x ≠ 0
⊢ f x * f x⁻¹ = 1
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:
ha,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 1 / 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⁻¹ = a ^ n * a⁻¹

Tactic:
rw [← zpow_add_one₀ ha, Int.sub_add_cancel]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ 1 * a ^ i = a * a ^ i

Tactic:
zpow_one

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a * a ^ i = a * a ^ i
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
rw [sqrt, toNat_natCast]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
ha : IsSquare a
⊢ IsSquare (a ^ n)

Tactic:
aesop (add simp Commute.mul_pow)

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
⊢ { toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } =
    { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ } * { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
by
    ext1 f
    exact mul_comp g₁ g₂ f

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

Goal state before:
pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
rw [h.eq, mul_ne_zero_iff] at this

Goal state after:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
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
⊢ 0 • a = 0

Tactic:
simp_rw [HSMul.hSMul, SMul.smul, Int.cast_zero]

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
⊢ 0 • a = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c

Tactic:
exact (h a bc.le).lt_of_ne (by rintro rfl; exact lt_irrefl _ bc)

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
rw [h]
    exact hb.le_add_tsub

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a ≤ a⁻¹ ↔ a ≤ 1

Tactic:
by contrapose!; exact inv_lt_self_iff

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

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

Tactic:
by
    have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
    rw [← mul_one (a ^ n), pow_succ]
    gcongr
    exact pow_nonneg ha₀ n

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
by
  simp only [le_antisymm_iff, pow_le_one_iff_of_nonneg ha hn, one_le_pow_iff_of_nonneg ha hn]

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
⊢ c * a < c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (d * b + d * a)).1 ?_
  calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
⊢ Contravariant { x // 0 < x } G₀ (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
rintro ⟨a, ha⟩ b c h

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
a : G₀
ha : 0 < a
b c : G₀
h : (fun x y ↦ y * ↑x) ⟨a, ha⟩ b ≤ (fun x y ↦ y * ↑x) ⟨a, ha⟩ c
⊢ b ≤ c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg.2 hb)

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 : r ≃r s
a b : β
⊢ s (f (f.symm a)) (f (f.symm b)) ↔ s a b

Tactic:
f.1.apply_symm_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ s a (f (f.symm b)) ↔ s a b
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑(y ^ n) = 1
hm : ↑(y ^ (m + 1)) = 1
⊢ ↑(y ^ (m + 1).gcd n) = 1

Tactic:
← Units.val_one (α := M),

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑(y ^ n) = ↑1
hm : ↑(y ^ (m + 1)) = ↑1
⊢ ↑(y ^ (m + 1).gcd n) = ↑1
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

Tactic:
by
  ext x; induction x <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLE α
h : c ≤ b
⊢ a - (b - c) = a + c - b

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h

Goal state after:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - (c + d - c) = a + c - (c + d)
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ 0 < a - b ↔ b < a

Tactic:
by rw [tsub_pos_iff_not_le, not_le]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - b) = min a b

Tactic:
rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ b⁻¹ * a < c

Tactic:
rw [mul_comm] at *
  exact mul_inv_lt_of_lt_mul₀ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ -⊤ = ⊤

Tactic:
ext; simp; simp [bot_eq_zero]

Goal state after: