mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
← prod_antidiagonal_swap

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤

Tactic:
or_iff_not_imp_right

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤

Tactic:
by
  rw [or_iff_not_imp_right]
  change _ ≠ _ → _
  rw [Ideal.ne_top_iff_one]
  intro h1
  rw [eq_bot_iff]
  intro r hr
  by_cases H : r = 0; · simpa
  simpa [H, h1] using I.mul_mem_left r⁻¹ hr

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * ↑1

Tactic:
cast_one,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * 1
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ span (range x) = ⨆ i, span {x i}

Tactic:
by
  rw [← span_iUnion, iUnion_singleton_eq_range]

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

Goal state before:
pp: α : Type u
f g : Filter α
⊢ f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Tactic:
simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})

Tactic:
by
  rw [← principal_singleton, comap_principal]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint (comap f G) F ↔ Disjoint G (map f F)

Tactic:
simp only [disjoint_iff, ← Filter.push_pull', map_eq_bot_iff]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
rw [← not_iff_not]
  simp only [not_frequently, eventually_bind]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ↑∅ = ⊥

Tactic:
Finset.coe_empty,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ∅ = ⊥
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
c : α
hb : f c ⋖ f a
⊢ False

Tactic:
rw [f.apply_covBy_apply_iff] at hb

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
c : α
hb : c ⋖ a
⊢ False
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R✝ : Type u_1
M : Type u_2
inst✝² : Semiring R✝
inst✝¹ : AddCommMonoid M
inst✝ : Module R✝ M
P Q R : { P // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
⊢ ⟨↑P ⊔ ↑Q, ⋯⟩ ≤ R

Tactic:
by
    rw [← Subtype.coe_le_coe] at hPR hQR ⊢
    exact sup_le hPR hQR

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = t.sup sp
⊢ s.FG

Tactic:
Finset.sup_eq_iSup,

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = ⨆ a ∈ t, sp a
⊢ s.FG
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α.ToType <i β.ToType

Tactic:
by
  apply Classical.choice (type_lt_iff.mp _)
  rwa [type_toType, type_toType]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a - 0 = a

Tactic:
simpa only [zero_add] using add_sub_cancel 0 a

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c

Tactic:
sub_lt_of_le hba

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a < b + c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : type s < (RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1) (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)

Tactic:
RelEmbedding.ofMonotone_coe,

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : type s < lift.{u, v} (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ (RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1) ((typein r).toRelEmbedding f.top) = type s

Tactic:
RelEmbedding.ofMonotone_coe,

Goal state after:
case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ lift.{u, v} ((typein r).toRelEmbedding f.top) = type s
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1
b n : ℕ
hb : n < b
h✝ : b ≤ 1
⊢ 0 = 0

Tactic:
| case1 =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card

Tactic:
refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
b : Ordinal.{u_1}
H : ∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ b.card
c : Cardinal.{u_1}
hc : c < a
⊢ c < b.card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

pp: case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
· rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]

Goal state after:
case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ (↑n).ord ≤ o ↔ ↑n ≤ o

Tactic:
Cardinal.ord_natCast

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o ↔ ↑n ≤ o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
· rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) = a ^ b * a

Tactic:
opow_of_ne_zero h

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) * a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ log 0 x = 0

pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0

Tactic:
· apply (csSup_of_not_bddAbove _).trans csSup_empty
    by_contra! hb
    refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)
    simp +contextual [one_le_iff_ne_zero]

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
have := l.nonempty_Iio.to_subtype

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (derivFamily f o) = derivFamily f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
m n : ℕ
hm : 1 < m
hn : n ≠ 0
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
rw_mod_cast [eq_comm, log_eq_iff (mod_cast hm) (mod_cast hn), ← Nat.log_eq_iff (.inr ⟨hm, hn⟩)]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

Tactic:
exact op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb✝ : b ∈ Iio (g o)
hb : b < g o
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb✝⟩ ≤ y

Tactic:
hg.lt_iff_exists_lt ho

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb✝ : b ∈ Iio (g o)
hb : ∃ a' < o, b < g a'
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb✝⟩ ≤ y
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case limit
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
hb : Order.IsSuccLimit b
IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
| limit b hb IH =>

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ o.cof.IsRegular

Tactic:
refine ⟨?_, (cof_ord_cof o).ge⟩
  rwa [aleph0_le_cof_iff, one_lt_cof_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := ⋯
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ LinearIndependent R v'

Tactic:
rw [linearIndependent_iffₛ]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ ∀ (l₁ l₂ : Option κ →₀ R), (linearCombination R v') l₁ = (linearCombination R v') l₂ → l₁ = l₂
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω_ c.ord = c.ord

Tactic:
by
  rw [← ord_aleph, hc.aleph_ord]

Goal state after:
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)

pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S

Tactic:
· apply iSup_le _
    intro i y hy
    exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Goal state after:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj

Tactic:
· rintro (⟨rfl, hxi⟩ | ⟨hi, hj⟩)
    · rw [eq_of_heq hxi]
    · rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]

Goal state after:
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → SMulZeroClass γ (β i)
inst✝¹ : (i : ι) → SMulZeroClass γᵐᵒᵖ (β i)
inst✝ : ∀ (i : ι), IsCentralScalar γ (β i)
r : γ
m : Π₀ (i : ι), β i
i : ι
⊢ (MulOpposite.op r • m) i = (r • m) i

Tactic:
by simp only [smul_apply, op_smul_eq_smul r (m i)]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
⊢ f i = 0 i

Tactic:
by_cases hs₂ : i ∈ s.val

Goal state after:
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∈ ↑s
⊢ f i = 0 i

case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∉ ↑s
⊢ f i = 0 i
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)

Tactic:
have H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset := Finset.inter_subset_left

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case snd
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i✝ : ι
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).2 i✝ = x.2 i✝

Tactic:
rw [comapDomain_apply, extendWith_some]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * χ (-a) = ψ a / χ a

Tactic:
map_neg_eq_inv,

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * (χ a)⁻¹ = ψ a / χ a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
γ : Type u_5
inst✝ : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ image2 f ↑{a} ↑t = ↑t

Tactic:
coe_singleton,

Goal state after:
α : Type u_1
γ : Type u_5
inst✝ : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ image2 f {a} ↑t = ↑t
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ = f * erase ag g₂
⊢ (erase ag g₁).coeff.support ∪ (erase ag g₂).coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase ag

Tactic:
simp [Finset.erase_union_distrib]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n * s) ≤ #s ^ n * #s
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ q ↔ Disjoint ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ q ↔ Codisjoint ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ q ↔ IsCompl ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl ↑⟨p, hp⟩ ↑⟨q, hq⟩
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ ((monomial n) c).coeffs = {c}

Tactic:
by
  rw [coeffs, support_monomial n hc]
  simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id).toFun ((lmapDomain R R g) l) ∈ span R (g '' ↑t1)

Tactic:
← Set.image_id (g '' ↑t1),

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id).toFun ((lmapDomain R R g) l) ∈ span R (id '' g '' ↑t1)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id) ((lmapDomain R R g) l) ∈ s

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (((lmapDomain R R g) l).sum fun i a ↦ a • id i) ∈ s