mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ c * b / d * d = c * b

Tactic:
div_mul_cancel₀ _ hd

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ c * b = c * b
Module: Mathlib.Algebra.Field.Defs

Goal state before:
pp: A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m

Tactic:
Rat.smul_def,

Goal state after:
A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ ↑m * 1 = ↑m
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
h.neg_pow,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ 1 ^ n = 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
h.neg_pow,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ -1 ^ n = -1
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a ≤ 1 * b ↔ a ≤ b

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ 1 * a ↔ b ≤ a

Tactic:
by rw [one_mul]

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

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

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
⊢ (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_7⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P

Tactic:
intros h P w

Goal state after:
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_7
w : x₁ = x₂ → y₁ = y₂ → P
⊢ P
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
a0 : 0 < a
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
by rw [one_mul]

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

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

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
b0 : 0 < b
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
by rw [one_mul]

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✝ a : G₀
ha : 0 < a
⊢ 0 < a⁻¹

Tactic:
apply lt_of_mul_lt_mul_left _ ha.le

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ a * 0 < a * a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ a * 0 < a * a⁻¹

Tactic:
apply lt_of_mul_lt_mul_left _ ha.le

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ a * (a * 0) < a * (a * a⁻¹)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
⊢ ∀ (a : α ↪ β), a = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ }

Tactic:
intro; ext v; exact isEmptyElim v

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
hb : b < 0
h : a < 1
⊢ b < a * b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
hb : b < 0
h : 1 < a
⊢ a * b < b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

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₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
simpa using one_le_inv_mul₀ ha (b := 1)

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₀
ha₀ : 0 < a
ha₁ : a ≤ 1
⊢ Antitone fun n ↦ a ^ n

Tactic:
refine antitone_int_of_succ_le fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

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 x ↦ x.toFun) f = (fun x ↦ x.toFun) g
⊢ f = g

Tactic:
by
    rcases f with ⟨⟨⟩⟩
    rcases g with ⟨⟨⟩⟩
    congr

Goal state after:
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₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
rw [mul_inv_le_iff₀ hc, mul_comm]

Goal state after:
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 * a ≤ b

Tactic:
le_div_iff₀' hc

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
⊢ c * a ≤ b ↔ c * a ≤ b
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₀
hb : 0 < b
hc : 0 < c
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
rw [div_le_iff₀ hb, div_le_iff₀' hc]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
by
  obtain ha | ha := le_or_gt 1 a <;> obtain hb | hb := le_or_gt 1 b
  · simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]
  · exact (lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim
  swap
  · simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]
  have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
    (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
    simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]
  refine this.mp ⟨fun h ↦ ?_, fun h ↦ by simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]⟩
  obtain ab | ab := le_or_gt (a * b) 1
  · refine (eq_one_of_inv_eq' ?_).le
    rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
  · rw [mabs_of_one_lt ab, mul_left_inj] at h
    rw [eq_one_of_inv_eq' h.symm] at ha
    cases ha.false

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 : α
⊢ b / a ⊔ (b / a)⁻¹ ⊔ 1 = |b / a|ₘ

Tactic:
← mabs,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |b / a|ₘ ⊔ 1 = |b / a|ₘ
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
⊢ map₂ f a none = none

Tactic:
by cases a <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (a ^ m ∈ Set.range fun x ↦ x ^ n) ↔ a ∈ Set.range fun x ↦ x ^ n

Tactic:
by
  simp [pow_eq_pow_iff_of_coprime hmn.symm]; aesop

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
⊢ map₂ f a 1 = 1

Tactic:
by cases a <;> rfl

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ f ↑x * f ↑x⁻¹ = 0

Tactic:
H,

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 0 * f ↑x⁻¹ = 0
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
⊢ (if h : b ≤ a then ⋯.choose else 0) ≤ c ↔ a ≤ c + b

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : b ≤ a
⊢ ⋯.choose ≤ c ↔ a ≤ c + b

case neg
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : ¬b ≤ a
⊢ 0 ≤ c ↔ a ≤ c + b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
⊢ map₂ f a ⊥ = ⊥

Tactic:
by cases a <;> rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : β
⊢ map₂ f a ↑b = map (fun x ↦ f x b) a

Tactic:
by cases a <;> rfl

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

Goal state before:
pp: m✝¹ n✝ k✝ : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc lbp k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + 1 + m

Tactic:
Nat.add_right_comm

Goal state after:
m✝¹ n✝ k✝ : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc lbp k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + m + 1
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = findGreatest P 0 ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n

Tactic:
Iff.comm

Goal state after:
case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
by
  obtain ⟨z, hlt⟩ := exists_lt (WithZero.unzero hx)
  rw [← WithZero.coe_lt_coe, WithZero.coe_unzero hx] at hlt
  exact ⟨z, WithZero.coe_ne_zero, hlt⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Tactic:
by rw [le_floor, Int.cast_zero]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simpa [WithTop.exists, WithTop.forall, exists_gt] using DenselyOrdered.dense

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ f ↑a * f ↑a⁻¹ = 0

Tactic:
H,

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ 0 * f ↑a⁻¹ = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case pos
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
simp [h, map_zero f]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
⊢ StrictMonoOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
by
  simp [StrictMonoOn, forall_and]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ q • f a = f ↑q * f a

Tactic:
Rat.smul_def,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ ↑q * f a = f ↑q * f a
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → ∀ (x : β), x ∈ t → x ∈ (fun b ↦ f a b) ⁻¹' u

Tactic:
mem_preimage

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a ^ 2 ↔ 1 ≤ |a|

Tactic:
simpa only [one_pow, abs_one] using sq_le_sq (a := 1) (b := a)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ (↑n + 1) * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)

Tactic:
refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n : ℕ
inst✝ : IsOrderedRing α
⊢ |a ^ n - b ^ n| ≤ |a - b| * ↑n * max |a| |b| ^ (n - 1)

Tactic:
obtain _ | n := n

Goal state after:
case zero
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * max |a| |b| ^ (0 - 1)

case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iio True = {False}

Tactic:
by aesop (add simp [Ioi, lt_iff_le_not_ge])

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Ioi False = {True}

Tactic:
by aesop (add simp [Ioi, lt_iff_le_not_ge])

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ (a + b) / 2 < b ↔ a < b

Tactic:
simp [div_lt_iff₀, mul_two]

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsLUB ∅ b
⊢ IsLUB ((fun a ↦ 0) '' ∅) 0

pp: case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB ((fun a ↦ 0) '' s) 0

Tactic:
· simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
      have hb := hs (b + b)
      rw [le_add_iff_nonneg_right] at hb
      exact hs.mono hb

Goal state after:
case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB ((fun a ↦ 0) '' s) 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
rw [mem_cons, mem_singleton]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0

case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf a (b :: l) = 0

Tactic:
rw [← e]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval * l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
by
  simp only [eval_cons, ← h, zpow'_add]
  ac_rfl

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : Monoid M
a : M
n✝ : ℕ
a✝ : ∀ {l : List M}, n✝ ≤ l.length → (∀ (a' : M), a' ∈ take n✝ l → Commute a a') → (l.insertIdx n✝ a).prod = a * l.prod
l : List M
hlen : n✝ + 1 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take (n✝ + 1) l → Commute a a'
⊢ (l.insertIdx (n✝ + 1) a).prod = a * l.prod

Tactic:
case succ i ih =>
    obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)
    simp only [insertIdx_succ_cons, prod_cons,
      ih (Nat.le_of_lt_succ hlen) (fun a' a'_mem => hcomm a' (mem_of_mem_tail a'_mem))]
    exact Commute.left_comm (hcomm hd (mem_of_mem_head? rfl)).symm tl.prod

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

Goal state before:
pp: case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

Tactic:
rintro rfl
    exact hnd (dvd_zero _)

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y

Tactic:
by
  rw [isRelPrime_comm] at H ⊢
  exact H.of_mul_left_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b