mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 (fun a b ↦ f (g a) (h b)) univ univ = (fun x ↦ f (g x.1) (h x.2)) '' univ

Tactic:
← image_prod,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ (fun x ↦ f (g x.1) (h x.2)) '' univ ×ˢ univ = (fun x ↦ f (g x.1) (h x.2)) '' univ
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
by
  grw [inter_comm, image2_inter_union_subset_union, image2_comm hf, union_self]

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

Goal state before:
pp: m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ m ≠ 2

Tactic:
rintro rfl

Goal state after:
n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
insert_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Icc a b \ ({a} ∪ {b}) = Ioo a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (t ∪ s) t

Tactic:
rw [union_comm]
  exact hc.union_left

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
insert_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {b} ∪ Ico a b = Icc a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
insert_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ {a} ∪ Ioo a b = Ico a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}

Tactic:
exact subset_sdiff_singleton hc hb

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
insert_eq,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
a b : List α
⊢ a = b → Forall₂ (fun x1 x2 ↦ x1 = x2) a b

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
a : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
⊢ l = [] → Forall₂ R [] l

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
⊢ l = [] → Forall₂ R l []

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
drop_left

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) l₂
⊢ Forall₂ R (drop l₁.length l) l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []

Tactic:
forall₂_nil_right_iff.1 hl1

Goal state after:
case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [insertIdx_of_length_lt hn₂]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod

Tactic:
by rw [map_id]

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
rintro rfl

Goal state after:
case mp
α : Type u
l₁ : List α
⊢ l₁.length = l₁.length ∧ ∀ (n : ℕ) (h₁ h₂ : n < l₁.length), l₁.get ⟨n, h₁⟩ = l₁.get ⟨n, h₂⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
intro ⟨h₁, h₂⟩
    exact ext_get h₁ h₂

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

Goal state before:
pp: q : ℚ
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₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Tactic:
exact (hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)

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

Goal state before:
pp: case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Tactic:
simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

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

Goal state before:
pp: p q : ℚ≥0
⊢ p = q → p.num = q.num ∧ p.den = q.den

Tactic:
rintro rfl

Goal state after:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))

Tactic:
push_cast

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (a * n) (a * d)) = ↑(divNat n d)

Tactic:
push_cast

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (n * a) (d * a)) = ↑(divNat n d)

Tactic:
push_cast

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
push_cast

Goal state after:
q : ℚ≥0
⊢ ↑q * ↑q.den = ↑q.num
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

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

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

Tactic:
ext; simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

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

Goal state after:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
z : α
hx : z ∣ x
hy : z ∣ y
h : ¬IsUnit z
⊢ z ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ 0 < q₁.den * q₂.den

Tactic:
by simp [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₂.den

Tactic:
Int.natCast_dvd_natCast

Goal state after:
case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ ↑q₁.den

Tactic:
Int.natCast_dvd_natCast

Goal state after:
case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₁.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 }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a 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 : ↑0 ≠ 0
e : divNat a 0 = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ False
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
push_cast

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.num) / ↑(q.den * r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.num * ↑r.num / (↑q.den * ↑r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.num * ↑r.den / (↑q.den * ↑r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Tactic:
push_cast

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.den * ↑r.num ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
push_cast

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.num * ↑q.num / (↑p.den * ↑q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Tactic:
push_cast

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.den * ↑q.den ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

Tactic:
push_cast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.num * ↑q.den / (↑p.den * ↑q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Tactic:
push_cast

Goal state after:
case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.den * ↑q.num ≠ 0
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2

Tactic:
← h3,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n1 * n2 * (e1 * e2) = t1 * t2
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1

Tactic:
← h3,

Goal state after:
α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * n2 * (e1 / e2) = t1
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ k / e = n

Tactic:
← h3,

Goal state after:
α : Type u_1
inst✝ : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ n * e / e = n
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
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
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

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
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
· rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]

Goal state after:
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
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
a : α
⊢ sSup s = a → IsLUB s a

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i

Tactic:
rw [Nat.sub_add_cancel hi]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ sSup (range fun i ↦ f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
minAx.sSup_inf_eq,

Goal state after:
α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ ⨆ a_1 ∈ range fun i ↦ f i, a_1 ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
⊢ ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)

Tactic:
← image_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
⊢ ⨆ d ∈ (fun x ↦ f x.1 x.2) '' s ×ˢ t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b

Tactic:
← image_prod,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup ((fun x ↦ f x.1 x.2) '' s ×ˢ t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ (⨅ i,
      ⨆ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j) ≤
    ⨆ b ∈ s, a ⊓ b

Tactic:
by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = sInf ((fun a ↦ ↑a) '' s)

Tactic:
by
  classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
rw [sSup_apply_eq_sSup_image]
    exact isLUB_csSup (image_nonempty.mpr hn) ((monotone_eval _).map_bddAbove hb)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨅ a, ⨆ b, f a b) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝

Tactic:
rw [iInf_iSup_eq]

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

Goal state before:
pp: case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
· exact ⟨b, hb⟩

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt

Goal state after:
case inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ico x y = Ico (e x) (e y)

Tactic:
← e.preimage_Ico,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' ⇑e ⁻¹' Ico (e x) (e y) = Ico (e x) (e y)
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

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 ↦ x1 ≤ x2) {a} ∧ IsLeast {a} a
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 ∧ IsGreatest s a

Tactic:
rintro rfl

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 ↦ x1 ≤ x2) {a} ∧ IsGreatest {a} a
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
obtain lt | lt := ha.lt_or_gt

Goal state after:
case inl
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : a < 0
⊢ Nontrivial { x // 0 ≤ x }

case inr
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial { x // 0 ≤ x }
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ a ⊓ a ⊓ ⨅ x, ⨅ (_ : p x), ↑(f x) = a ⊓ ⨅ x, ⨅ (_ : p x), ↑(f x)

Tactic:
inf_idem

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
hn : ↑0 ≠ 0
⊢ False
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)

Tactic:
exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : Group α
a b : α
⊢ (a ⊓ b)⁺ᵐ = a⁺ᵐ ⊓ b⁺ᵐ

Tactic:
by
  simp [oneLePart, sup_inf_right]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)

Tactic:
rw [pow_succ']

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

Goal state before:
pp: n k : ℕ
⊢ 0 < n.descFactorial k ↔ k ≤ n

Tactic:
by simp [Nat.pos_iff_ne_zero]

Goal state after: