mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - a

Tactic:
tsub_self,

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : LE α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊤
x✝ : y ≤ z
⊢ x + y ≤ x + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊤
x✝ : x ≤ y
⊢ x + z ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightMono α
hw : w ≠ ⊤
hwy : w ≤ y
hxz : x < z
⊢ w + z ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftMono α
inst✝ : AddRightStrictMono α
hx : x ≠ ⊤
hwy : w < y
hxz : x ≤ z
⊢ y + x ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
· rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ 0 • a = 0

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]; cases a <;> simp [zero_nsmul]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
by gcongr

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
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:
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.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithBot α
inst✝² : LE α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
x✝ : y ≤ z
⊢ x + y ≤ x + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithBot α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊥
x✝ : x ≤ y
⊢ x + z ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithBot α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightMono α
hw : w ≠ ⊥
hwy : w ≤ y
hxz : x < z
⊢ w + z ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithBot α
inst✝² : Preorder α
inst✝¹ : AddLeftMono α
inst✝ : AddRightStrictMono α
hx : x ≠ ⊥
hwy : w < y
hxz : x ≤ z
⊢ y + x ≤ y + z

Tactic:
by gcongr

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

Goal state before:
pp: case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)

Tactic:
exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

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

Tactic:
Nat.cast_one

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a < 1 ↔ a < 1
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
⊢ a ≤ ↑⌊a⌋₊ + ↑1

Tactic:
Nat.cast_one

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a ≤ ↑⌊a⌋₊ + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rw [floor_lt ha]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < ↑⌈b⌉₊
Module: Mathlib.Algebra.Group.Invertible.Defs

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

Tactic:
rw [← mul_assoc, invOf_mul_self, one_mul]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) ≤ b ^ (n + 1)

Tactic:
by gcongr

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ b ^ (n + 1) ≤ a ^ (n + 1)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ -c ↔ a ∣ c

Tactic:
dvd_neg

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c ↔ a ∣ c
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b

Tactic:
rw [← h ha, ← h hb]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b

Tactic:
rw [← h ha, ← h hb]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
⊢ f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image Hst ha.1 ha.2

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
s : Set α
h : s.Nonempty
⊢ Minimal (fun x ↦ x ∈ s) (⋯.min s h)

Tactic:
grind [Minimal, lt_iff_le_not_ge, WellFounded.min]

Goal state after:
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 (⇑f ⁻¹' s) x ↔ IsLUB s (f x)

Tactic:
← f.symm_symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (⇑f.symm.symm ⁻¹' s) x ↔ IsLUB s (f.symm.symm 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)
hts : ¬IsCofinalFor t s
⊢ IsCofinalFor s t

Tactic:
x

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a

Tactic:
by
    rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
    · exact h₁.symm ▸ le_sup_left
    obtain ⟨y, lty, ylt⟩ := exists_between h₂
    apply (not_lt_of_ge (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
    obtain ⟨u, au, ub⟩ := exists_between h
    apply (hx ⟨au, ub⟩).trans ub.le

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑n * ⅟↑d

Tactic:
of_decide_eq_true h

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑n * ⅟↑d

Tactic:
of_decide_eq_true h

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ l.insertIdx n a ⊆ a :: l

Tactic:
intro b hb

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ l.insertIdx n a
⊢ b ∈ a :: l
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Tactic:
by
  simp [getElem_insertIdx_add_succ, hk']

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ l.set n a ~ a :: l.eraseIdx n

Tactic:
← insertIdx_eraseIdx_self (Nat.ne_of_lt h)

Goal state after:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a ~ a :: l.eraseIdx n
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩

Goal state after:
case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁✝ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁✝ v
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
⊢ l₁ ⊆ l₂

Tactic:
x

Goal state after:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
⊢ x ∈ l₁ → x ∈ l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n

Tactic:
map_singleton,

Goal state after:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a ↑n = a ^ n

Tactic:
rw [zpow'_of_ne_zero_right]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n

case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝ : Inhabited α
hl : l₁.length = l₂.length
h : ∀ (n : ℕ), l₁[n]! = l₂[n]!
n : ℕ
h₁ : n < l₁.length
h₂ : n < l₂.length
⊢ l₁[n] = l₂[n]

Tactic:
by simpa only [← getElem!_pos] using h n

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

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ * (d₂ /. n₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
divInt_mul_divInt

Goal state after:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ * d₂ /. (d₁ * n₂) = n₁ * d₂ /. (d₁ * n₂)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
simpa using! congr_arg num hab

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
rw [mul_comm]
  apply mul_right_dvd

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₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
eq_div_iff_mul_eq d₂a,

Goal state after:
α : 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₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ * ↑d₂ = ↑n₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
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:
e

Goal state after:
α : 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) = ↑(n * b)
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
    exact mul_ne_zero hq hr

Goal state after:
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
    exact mul_ne_zero hq hr

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ ↑d ∣ b

Tactic:
e

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b
⊢ ↑d ∣ b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ ↑d ∣ b

Tactic:
rwa [e] at dd

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑b = ↑d * ↑k

Tactic:
ke,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑(↑d * k) = ↑d * ↑k
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
    exact mul_ne_zero hq hr

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

Goal state before:
pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
have : (n : ℚ) ≠ 0 := by rwa [← intCast_inj]  at hn
    simp only [Int.ediv_self hn, Int.cast_one, div_self this]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹

Tactic:
tsub_mul

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
a b : α
inst✝ : Fact (a < b)
x y : ↑(Ioc a b)
⊢ Codisjoint x y ↔ ↑x ⊔ ↑y = b

Tactic:
by
  simp [_root_.codisjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ Codisjoint x y ↔ Codisjoint ↑x ↑y

Tactic:
by
  simp [_root_.codisjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : SemilatticeSup α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ Codisjoint x y ↔ ↑x ⊔ ↑y = b

Tactic:
by
  simp [_root_.codisjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
a : α
x✝ : a ∈ s
⊢ a ∆ sSup t ≤ ⨆ b ∈ t, a ∆ b

Tactic:
simpa [sSup_image] using symmDiff_sSup_le ht

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ sSup (⋃ i, Iic (f i)) = ⨆ i, f i

Tactic:
apply csSup_eq_csSup_of_forall_exists_le
  · rintro x ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨f i, mem_range_self _, hi⟩
  · rintro x ⟨i, rfl⟩
    exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

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

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c

Tactic:
exact hb hc

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

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ s ⊆ {⊤}

Tactic:
intro b hb

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ b ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b

Tactic:
intro b hb

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ Iio b = Ico a b

Tactic:
Ici_inter_Iio

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ico a b = Ico a b
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % b = ↑r

Tactic:
← Int.emod_neg,

Goal state after:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % -b = ↑r
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!

Tactic:
rw [factorial_one]
    exact lt_factorial_self (succ_le_succ hi)

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

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k)! * n.descFactorial k = n !

Tactic:
factorial_mul_descFactorial (le_trans hkm hmn)

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ n ! = n !
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
by
  rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
  refine le_trans ?_ (sub_one_lt_floor _).le
  rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
  exact floor_le _

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n

Tactic:
have hn' : 0 < (n : k) := by
    norm_cast

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n