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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular (a * b)

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLE α
h : c ≤ b
⊢ a - (b - c) = a + c - b

Tactic:
by
  obtain ⟨d, rfl⟩ := exists_add_of_le h
  rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

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 n : ℤ
⊢ m ≤ n → ↑m ≤ ↑n

Tactic:
h

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = unbotD d ⊥ ↔ x = ⊥ ∨ x = ↑d ∧ ⊥ = ⊥ ∨ x = ⊥ ∧ ⊥ = ↑d

Tactic:
simp [unbotD_eq_iff, or_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
d : α
x : WithBot α
a✝ : α
⊢ unbotD d x = unbotD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = ⊥ ∨ x = ⊥ ∧ ↑a✝ = ↑d

Tactic:
simp [unbotD_eq_iff, or_comm]

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

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

Tactic:
h

Goal state after:
case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P 0
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:
by rw [Nat.cast_one]

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
⊢ ↑0 < a ↔ 0 < a

Tactic:
Nat.cast_zero

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

Tactic:
Nat.cast_zero

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a ≤ 0 ↔ a ≤ 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
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 : a < 0
⊢ ↑0 < b

Tactic:
Nat.cast_zero

Goal state after:
case inr
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 : a < 0
⊢ 0 < b
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
⊢ Nat.cast ⁻¹' Iic a = Iic ⌊a⌋₊

Tactic:
ext
  simp [le_floor_iff, ha]

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

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

Tactic:
by
  rw [← mul_assoc, invOf_mul_self, one_mul]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b

Tactic:
by
  have := hf.forall_le_of_antitone hf' le_rfl
  exact le_antisymm (this a b) (this b a)

Goal state after:
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 : -1 = ⅟a * b + ⅟b * a
⊢ -a = a * (⅟a * b + ⅟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✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ (Equiv.divRight₀ a ⋯) b ≤ (Equiv.divRight₀ a ⋯) c ↔ b ≤ c

Tactic:
by
    simp only [Equiv.divRight₀_apply, div_eq_mul_inv]
    exact mul_le_mul_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

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
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n

Tactic:
gcongr <;> try assumption

Goal state after:
case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬(s.Nonempty ∧ t.Nonempty) ↔ s = ∅ ∨ t = ∅

Tactic:
not_and_or

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
    sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

Goal state after:
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
a : β
⊢ f a = g a

Tactic:
apply WellFoundedLT.induction 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 : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ (fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) ((fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ⟨rangeSplitting f y, ⋯⟩) = ⟨rangeSplitting f y, ⋯⟩

Tactic:
simp [apply_rangeSplitting f]

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_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑s
⊢ (fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) x) = x

Tactic:
simp [apply_rangeSplitting f]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ f ((ofInjective f hf).symm ⟨f x, ⋯⟩) = f (rangeSplitting f ⟨f x, ⋯⟩)

Tactic:
simp [apply_rangeSplitting f]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLeast (upperBounds s) a ↔ IsLeast (upperBounds t) a

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLeast (upperBounds t) a ↔ IsLeast (upperBounds t) a
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
⊢ Subsingleton (α ≃o β)

Tactic:
by
  refine ⟨fun f g ↦ ?_⟩
  rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]

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

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x ↦ ∀ y ∈ s, y ≤ x

Tactic:
exact Monotone.ball fun x _ => monotone_le

Goal state after:
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 ≤ ↑n

Tactic:
exact Nat.cast_nonneg' n

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a + -b = c

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ c = c
Module: Mathlib.Control.Functor

Goal state before:
pp: γ : Type u_1
⊢ LawfulFunctor (Const γ)

Tactic:
constructor <;> intros <;> rfl

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
⊢ tail^[n + 1] l = drop (n + 1) l

Tactic:
cases l <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (drop (n + 1) (a✝ :: l₁✝)) (drop (n + 1) (b✝ :: l₂✝))

Tactic:
by simp [And.intro h₁ h₂, forall₂_drop n]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : d < 0
⊢ d ≤ c

pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c

Tactic:
· exact hd.le.trans hc

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ε⁻¹ * ((ε * a) ^ 2 + b ^ 2) = ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
mul_pow,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ε⁻¹ * (ε ^ 2 * a ^ 2 + b ^ 2) = ε * a ^ 2 + ε⁻¹ * b ^ 2
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
by
  cases Nat.lt_or_ge m l₁.length with
  | inl hm =>
    rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
    cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]
  | inr hm =>
    rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
    rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
by
  rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
  suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
    simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
  trans ∀ c, c ∈ l → c = b ∨ c = a
  · simp [subset_def, or_comm]
  · exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * (map f as).prod = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Tactic:
h

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * l₂.eval = l.eval

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ l.eval = l.eval
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval / l₂.eval = l.eval

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ l.eval = l.eval
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
⊢ t.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
⊢ t'.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take (i + 1) L).prod = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (Nat.le_of_lt h₁)] at this

Goal state after:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
by
  have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
  rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * 1⁻¹

Tactic:
inv_one,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * 1
Module: Mathlib.Data.Rat.Defs

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

Tactic:
by
    rw [divInt_add_divInt _ _ h h, divInt_eq_divInt_iff h (Int.mul_ne_zero h h)]
    simp [Int.add_mul, Int.mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
x y : α
inst✝ : Nontrivial α
h : IsRelPrime x y
⊢ x = 0 → y ≠ 0

Tactic:
by rintro rfl rfl; exact not_isRelPrime_zero_zero h

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
⊢ m * n ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Tactic:
h

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ IsUnit a

Tactic:
have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ IsUnit a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
add_def,

Goal state after:
q₁ q₂ : ℚ
⊢ (normalize (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) (q₁.den * q₂.den) ⋯).den ∣ q₁.den.lcm q₂.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.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
add_def,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den)) = ↑q + ↑r
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
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
h

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
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ l * n ^ e2 * e1 ^ e2 = l * (n * e1) ^ e2

Tactic:
mul_pow,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ l * n ^ e2 * e1 ^ e2 = l * (n ^ e2 * e1 ^ e2)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: k e : ℕ
h : Nat.rawCast 1 = e
⊢ k.rawCast = e * k

Tactic:
by simp [← h]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a e : R
h : Nat.rawCast 1 = e
⊢ a ^ 0 = e + 0

Tactic:
by simp [← h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ i, g ↑i = ⨆ i, g (f i)

Tactic:
iSup_range'

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ i, g (f i) = ⨆ i, g (f i)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (f (sSup x✝))

Tactic:
map_sSup

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (⨆ a ∈ x✝, f a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

Tactic:
simp only [sdiff_subset_iff, ← biUnion_union]
  apply biUnion_subset_biUnion_left
  rw [union_sdiff_self]
  apply subset_union_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j

Tactic:
simp_rw [mem_iUnion, iSup_exists]

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
⊢ ↑⊥ = ⊥

Tactic:
coe_bot

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
⊢ ⊥ = ⊥
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s

Tactic:
· apply csSup_le t_ne (fun y hy ↦ ?_)
      rcases ht y hy with ⟨x, xs, hyx⟩
      exact hyx.trans (le_csSup Bs xs)

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

Goal state before:
pp: case mp.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
exact H hx hy hne

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

Goal state before:
pp: α : Type u_6
β : Type u_7
f : α → Set β
⊢ (range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)

Tactic:
aesop (add simp [PairwiseDisjoint, Set.Pairwise])

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ f x.1 x.2 ∈ f y.1 '' t

Tactic:
h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ f y.1 '' t