mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
f : β → M
hf : StrictMono f
x✝ : 1 ≠ 0
⊢ StrictMono fun x ↦ f x ^ 1

Tactic:
by simpa

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

Goal state before:
pp: case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : (a * b)⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b

Tactic:
mul_inv_rev,

Goal state after:
case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : b⁻¹ * a⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
mul_inv_rev,

Goal state after:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |b|ₘ⁻¹⁻¹ * |a|ₘ⁻¹ ≤ |a / b|ₘ
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 c : G
hab : a ≤ b
hbc : b ≤ c
⊢ b⁻¹ ≤ max |a|ₘ |c|ₘ

Tactic:
simp [(inv_le_inv_iff.mpr hab).trans (inv_le_mabs a)]

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 : G
⊢ |a / a|ₘ ≤ 1

Tactic:
rw [div_self', mabs_one]

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 : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹

Tactic:
mul_inv_rev,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
sup_right_idem,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c * ((b ⊓ a) * c)⁻¹ = (b ⊔ a) / (b ⊓ a)

Tactic:
mul_inv_rev,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c * (c⁻¹ * (b ⊓ a)⁻¹) = (b ⊔ a) / (b ⊓ a)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n % k * (m * r % k) % k = r % k

Tactic:
← mul_mod,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * (m * r) % k = r % k
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ min (a * b) c = min (min a c * min b c) c

Tactic:
by
  simpa [min_comm _ c] using min_mul_distrib c a b

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ -a = b

Tactic:
have ha : a ≠ ⊤ := by rintro rfl; simp at h

Goal state after:
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a = b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ -b ≠ ⊤

Tactic:
by simpa

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

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x

Tactic:
· rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : LT α
⊢ x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]

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

Goal state before:
pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
simpa [none_eq_top, some_eq_coe, ← coe_add] using fun a ↦ ha a

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

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

Tactic:
rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b

Tactic:
ha.tsub_le_tsub_iff_left hb hba,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b ≤ a - c ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
change dite _ _ _ ≤ c ↔ _

Goal state after:
α : 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
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithBot α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊥
⊢ x + y = x + z ↔ y = z

Tactic:
by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩
  induction a
  · rwa [zero_add, zero_add]
  induction b
  · rw [add_zero]
    induction c
    · rw [add_zero]
    · rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)
  · rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
    rw [← coe_add, ← coe_add _ c, coe_le_coe]
    gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
⊢ b < c

Tactic:
have := h.ne_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
⊢ b < c
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
use e i
    simp [Function.extend_apply' _ _ _ hb]

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

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ n ≤ FloorSemiring.floor a ↔ n ≤ FloorSemiring.floor a

Tactic:
rw [H₁.gc_floor, H₂.gc_floor] <;> exact h

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

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

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
rw [image2_swap g, image2_swap g']
  exact image2_assoc fun _ _ _ => h_right_comm _ _ _

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

Goal state before:
pp: a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ 0 < |b|

Tactic:
by simpa

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

Goal state before:
pp: a b : ℤ
h₁ : b ≠ 0
h₂ : a ∣ b
⊢ a ∣ |b|

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s

Tactic:
by rw [image_subset_iff, image_eq_preimage_symm]

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ Disjoint s {a}

Tactic:
by simpa

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

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

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁

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

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

Tactic:
by simpa

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

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

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc

Tactic:
show Int.mul (-nb) _ = _ from neg_mul ..

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Iio 0)

Tactic:
convert! sub_inv_antitoneOn_Iio (α := α)
  exact (sub_zero _).symm

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l

Tactic:
rwa [hf y]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = fun x1 x2 ↦ x1 ~ map f x2

Tactic:
conv_rhs => rw [← Relation.comp_eq_fun (map f)]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = Perm ∘r fun x1 x2 ↦ x1 = map f x2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case e_head
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ = head✝

Tactic:
subsingleton

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.head? = l.head?

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Goal state after:
α : Type u
l : List α
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ l).flatten.head? = l.head?
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 0 n = 0

Tactic:
by
  simp +contextual only [zpow', true_and, ite_eq_left_iff]
  intro hn
  exact zero_zpow n hn

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

Goal state before:
pp: α : Type u
k : ℕ
l : List α
h : k ≠ 0
hk : k < l.length
⊢ l[k] ∈ l.tail

Tactic:
cases l <;> grind

Goal state after:
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:
simp only [eval_cons, ← h, zpow'_add]
  ac_rfl

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
prod_range_div'

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ f 0 / f n = f 0 / f n
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w } = 0

Tactic:
by congr; simp_all

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
h : ∀ (x : α), x ∈ l → f x = some (g x)
⊢ ∀ (x : α), x ∈ l → f x = (some ∘ g) x

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ Forall p (x :: l) → Forall q (x :: l)

Tactic:
by
    simp only [forall_cons, and_imp]
    rw [← and_imp]
    exact And.imp (h x) (Forall.imp h)

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑(divNat q.num q.den) = ↑q

Tactic:
by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a * b⁻¹ * (c * d⁻¹) = a * c * (d⁻¹ * b⁻¹)
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)

Tactic:
· rwa [zero_mul]

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₁ ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₂ ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹

Tactic:
simp only [Rat.neg_divInt, Rat.inv_divInt, Rat.divInt_neg]

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

Goal state before:
pp: b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b

Tactic:
rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
    intCast_div_self, Int.cast_mul, mul_div_assoc]

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ {n : ℕ},
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1) =
    ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1)

Tactic:
by simpa

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ (n : ℕ),
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0

Tactic:
by simpa

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

Goal state before:
pp: case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c

Tactic:
apply h.eq_tsub_of_add_eq
    rw [← mul_add, tsub_add_cancel_of_le hcb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLinearOrder α
a : α
s : Set β
f : β → α
⊢ a < ⨆ i ∈ s, f i ↔ ∃ i ∈ s, a < f i

Tactic:
by
  simp [lt_iSup_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ sSup {a} = a

Tactic:
sSup_singleton

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ a = a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
by_cases h : p

Goal state after:
case pos
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

case neg
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : ¬p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ j, extend e f ⊥ j = ⨆ i, f i

Tactic:
by
  rw [iSup_split _ fun j => ∃ i, e i = j]
  simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Monotone (f i)
⊢ ∀ f_1 ∈ range fun i ↦ f i, Monotone f_1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Antitone (f i)
⊢ ∀ f_1 ∈ range fun i ↦ f i, Antitone f_1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ i, ↑i)

Tactic:
exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

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

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
⊢ {x | p a x ∧ q x b} ∩ {y | r y ↑c} = {y | p a y ∧ r y ↑c}

Tactic:
ext; simp +contextual [h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Tactic:
by
  simpa only [disjoint_comm] using @sSup_disjoint_iff

Goal state after: