mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
· rw [mul_inv]
    exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝³ : (i : ι) → Group (α i)
f : (i : ι) → α i
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), MulLeftMono (α i)
inst✝ : ∀ (i : ι), MulRightMono (α i)
h : f = 1
i : ι
⊢ |f|ₘ i = 1 i

Tactic:
by simp [h]

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

Goal state before:
pp: x y : ℕ
this : x.P y (x.gcd y, x.xgcd y)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
xgcd_val

Goal state after:
x y : ℕ
this : x.P y (x.gcd y, x.gcdA y, x.gcdB y)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
⊢ (∃ c, a = c ^ n ∧ b = c ^ m) → a ^ m = b ^ n

Tactic:
by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
· exact ⟨0, by have := h.symm; simp_all⟩

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : a = ⊤
⊢ -a = ⊤

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m : ℤ
⊢ ∀ ⦃b : ℤ⦄, m ≤ b → ↑m ≤ ↑b

Tactic:
n

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
⊢ m ≤ n → ↑m ≤ ↑n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m✝ n✝ k : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → y.lbp m → (∀ (n : ℕ), n < y → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p n

Tactic:
rw [e]

Goal state after:
m✝ n✝ k : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → y.lbp m → (∀ (n : ℕ), n < y → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p m
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : ↑(unzero ha) < ↑(ofAdd b)
⊢ toAdd (unzero ha) < b

Tactic:
coe_lt_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : unzero ha < ofAdd b
⊢ toAdd (unzero ha) < b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ ↑(unzero ha) < ↑(ofAdd b)

Tactic:
coe_lt_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ unzero ha < ofAdd b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝

Tactic:
simpa using le_inf

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ a✝² ≤ a✝¹ → a✝² ≤ a✝ → a✝² ≤ a✝¹ ∧ a✝² ≤ a✝

Tactic:
simpa using le_inf

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
⊢ n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a

Tactic:
by
  rw [← Nat.lt_ceil, Nat.add_one_le_iff]

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟b * ⅟a * (a * b) = 1

Tactic:
by simp [← mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ a * b * (⅟b * ⅟a) = 1

Tactic:
by simp [← mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝³ : Monoid α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a * b)
⊢ a * b * (⅟b * ⅟a) = 1

Tactic:
by simp [← mul_assoc]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
⊢ FloorSemiring.floor = FloorSemiring.floor

Tactic:
ext a

Goal state after:
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
⊢ FloorSemiring.floor a = FloorSemiring.floor a
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
h : -a = b + a * ⅟b * a
⊢ -(b + a) = a * ⅟b * a

Tactic:
by simp [h]

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulRight₀ c hc).map_sup a b

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + x * y ^ n + y * y ^ n + y * x ^ n

Tactic:
add_assoc (x * x ^ n) (x * y ^ n),

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + (x * y ^ n + y * y ^ n) + y * x ^ n
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

Tactic:
refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.1 ≤ a

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.2 ≤ a

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
⊢ False

Tactic:
refine hm ⟨_, fun y hy => ?_⟩

Goal state after:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
⊢ Acc r y
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
⊢ f = g

Tactic:
ext a

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a : β
⊢ f a = g a
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ id ≤ f

Tactic:
Pi.le_def

Goal state after:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ ∀ (i : β), id i ≤ f i
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB s (f (f.symm x)) ↔ IsLUB s x

Tactic:
f.apply_symm_apply

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB s x ↔ IsLUB s x
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ IsCofinalFor t s ∨ IsCofinalFor s t

Tactic:
rw [or_iff_not_imp_left]

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ ¬IsCofinalFor t s → IsCofinalFor s t
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzt : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
· exact ⟨z, hzt, hxz⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type ?u.3
inst✝¹ : Semiring α
a k b : ℕ
inst✝ : Invertible ↑a
h : a = k * b
⊢ ↑a = ↑k * ↑b

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
by rw [lt_div_iff₀ hb, one_mul]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
x✝ : l.length < n ∨ l.length ≥ n
⊢ a = b ∨ a ∈ l

Tactic:
cases Nat.lt_or_ge (length l) n with

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
by
  simp only [eval_cons, ← h, zpow'_neg, div_eq_mul_inv, mul_inv, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval

Tactic:
rw [eval_cons, eval_cons, ← h]
  ac_rfl

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

Goal state before:
pp: M : Type u_4
inst✝² : Monoid M
inst✝¹ : BEq M
inst✝ : LawfulBEq M
l : List M
⊢ (filter (fun x ↦ x != 1) l).prod = l.prod

Tactic:
induction l <;> grind

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

Goal state before:
pp: case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * ((take n L).prod * (L[n]⁻¹ * (drop n L).prod)) = L.prod * (L[n]⁻¹ * a)

Tactic:
mul_comm _ (drop n L).prod,

Goal state after:
case pos
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ a * ((take n L).prod * ((drop n L).prod * L[n]⁻¹)) = L.prod * (L[n]⁻¹ * a)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
rw [mul_def]

Goal state after:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten

Tactic:
· cases i <;> simp [take_length_add_append, *]

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
ne_comm,

Goal state after:
⊢ 1 ≠ 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
by simp [h]

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

Goal state before:
pp: a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Tactic:
simp [Rat.mkRat_eq_div]

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ q.toNNRat ≤ p.toNNRat ↔ q ≤ p

Tactic:
simp [← coe_le_coe, toNNRat, hp]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
SemiconjBy,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
SemiconjBy,

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den

Tactic:
c_mul_num,

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ (q * r).num * ↑q.den * ↑r.den = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den

Tactic:
by
  let s := q.num * r.num /. (q.den * r.den : ℤ)
  have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
  obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.num) hs
  rw [c_mul_num, mul_assoc, mul_comm]
  nth_rw 1 [c_mul_den]
  rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]
  intro
  have h : _ = s := divInt_mul_divInt q.num r.num
  rw [num_divInt_den, num_divInt_den] at h
  rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den

Tactic:
c_mul_num,

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ (q + r).num * ↑q.den * ↑r.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑(n * b) = ↑(a * d)

Tactic:
rw [e]

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

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : FunLike F ℚ≥0 α
inst✝ : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
⊢ f q = ↑q

Tactic:
rw [← map_nnratCast f, NNRat.cast_id]

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: p : ℚ → Prop
h : ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)
q : ℚ
⊢ p q

Tactic:
by simpa [num_div_den] using h q.num q.den (mod_cast q.den_ne_zero)

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

Goal state before:
pp: ⊢ {0} ∪ range succ = univ

Tactic:
ext n
  cases n <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ ⨆ b, f b = f true ⊔ f false

Tactic:
by
  rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b

Tactic:
← (h₂ _).le_iff_le,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ ¬g a (f a) ≤ rhs

Tactic:
simpa using hf a

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:

Tactic:
_ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ∈ lowerBounds (f '' Icc a b)
⊢ a ∈ Icc a b ∧ f a = f a

Tactic:
by simp [hab]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
s : Set (WithTop α)
h : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
s : Set (WithBot α)
h : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsLeast s a

Tactic:
rintro rfl
    exact ⟨IsAntichain.singleton, isLeast_singleton⟩

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = insert x (mulSupport f)

Tactic:
ext a

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
⊢ mulSupport (update f x 1) = mulSupport f \ {x}

Tactic:
ext a

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint (mulSupport (mulSingle i a)) (mulSupport (mulSingle j b)) ↔ i ≠ j

Tactic:
mulSupport_mulSingle_of_ne ha,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint {i} (mulSupport (mulSingle j b)) ↔ i ≠ j
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ * a⁺ᵐ = |a|ₘ

Tactic:
rw [oneLePart_def, mul_sup, mul_one, leOnePart_def, sup_mul, one_mul, inv_mul_cancel, sup_assoc,
    ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
  exact sup_eq_left.2 <| one_le_mabs a

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!

Tactic:
rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]

Goal state after:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : ↑q.num ≠ 0
⊢ ↑(q ^ z) = ↑q ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · simp
  · simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]
    congr
    rw [cast_inv_of_ne_zero hq]

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

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 2⁻¹ = 1

Tactic:
norm_num [round_eq_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round (-2⁻¹) = 0

Tactic:
norm_num [round_eq_iff]

Goal state after: