mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
a : γ
⊢ f (Sum.inl a) = Sum.inl a

Tactic:
simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a

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

Goal state before:
pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o = (lift.{u, v} o).pred

Tactic:
eq_comm,

Goal state after:
case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ (lift.{u, v} o).pred = lift.{u, v} o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ range (familyOfBFamily' r ho f) → a ∈ o.brange f

Tactic:
rintro ⟨b, rfl⟩
    apply mem_brange_self

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

Goal state before:
pp: case pos
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
exact isNormal_ord.map_sSup hn hs

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u, u + 1} (typeLT ↑(Iio o))

Tactic:
lift_id'.{u, u + 1},

Goal state after:
o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = typeLT ↑(Iio o)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
⊢ Function.swap (fun x1 x2 ↦ x1 * x2) ⟦{ α := γ, r := t, wo := wo✝ }⟧ ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤
    Function.swap (fun x1 x2 ↦ x1 * x2) ⟦{ α := γ, r := t, wo := wo✝ }⟧ ⟦{ α := β, r := s, wo := wo✝¹ }⟧

Tactic:
by
      refine
        (RelEmbedding.ofMonotone (fun a : γ × α => (a.1, f a.2)) fun a b h => ?_).ordinal_type_le
      obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
      · exact Prod.Lex.left _ _ h'
      · exact Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False

Tactic:
rw [h] at this

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
rw [← mul_le_iff_le_div hc]
    exact (mul_div_le a c).trans h

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ ¬r ((enum r) ⟨(#↑s).ord, ⋯⟩) (⋯.min sᶜ h)

Tactic:
grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 1) = 0 ^ b * 0

Tactic:
zero_opow (add_pos_of_right zero_lt_one b).ne',

Goal state after:
case inl
b : Ordinal.{u_1}
⊢ 0 = 0 ^ b * 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ n < b ^ log b (n + 1)

Tactic:
simp [H]

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

Goal state before:
pp: b n k : ℕ
⊢ log b (n / b ^ k) = log b n - k

Tactic:
induction k with
  | zero => grind
  | succ k hk => rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, log_div_base, hk, sub_add_eq]

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

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
div_le hn',

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m < ↑n * succ ↑(m / n)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
obtain rfl | ha := eq_zero_or_pos a
  · obtain rfl | hc := eq_zero_or_pos c; · simp
    have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
    rw [zero_opow hc.ne', zero_opow, mul_zero]
    exact (hc.trans_le le_add_self).ne'
  obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt; · simp
  induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)

Tactic:
refine l.le_iff_forall_le.2 fun x hx => le_of_lt ?_

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ x < ω * (a / ω)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
rwa [opow_le_iff_le_log' hb hc]

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

Goal state before:
pp: case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a

Tactic:
exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ i, fixedPoints (f i))

Tactic:
eq_comm,

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ enumOrd (⋂ i, fixedPoints (f i)) = derivFamily f
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) b = a * ω + b

Tactic:
by
  revert b
  rw [← funext_iff, IsNormal.ext_iff (isNormal_deriv _) (isNormal_add_right _)]
  refine ⟨?_, fun a h => ?_⟩
  · rw [bot_eq_zero, deriv_zero_right, add_zero]
    exact nfp_add_zero a
  · rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]
    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

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

Goal state before:
pp: case ind.mk.hab
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := ⋯
f : α × α ↪ Lex (α × Lex (α × α)) := ⋯
s : α × α → α × α → Prop := ⋯
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding p).card ≤ #↑(Iio q) * #↑(Iio q)

Tactic:
apply (Set.embeddingOfSubset { x | s x p } ..).cardinal_le.trans_eq (mk_setProd ..)

Goal state after:
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := ⋯
f : α × α ↪ Lex (α × Lex (α × α)) := ⋯
s : α × α → α × α → Prop := ⋯
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ {x | s x p} ⊆ Iio q ×ˢ Iio q
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (ω_ o) = ω_ (Ordinal.lift.{v, u} o)

Tactic:
by
  simp [omega_eq_preOmega]

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c

Tactic:
← aleph0_le_preAleph,

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ℵ₀ ≤ preAleph (preAleph.symm c)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ cof 1 = 1

Tactic:
by
  simpa using cof_add_one 0

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

Goal state before:
pp: case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
rw [← Ne] at h2a

Goal state after:
case neg.inr.inr
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)

Goal state after:
case refine_1.inr.inl
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ 0 ∈ Set.range fun x ↦ ω ^ ω ^ x

case refine_1.inr.inr
a : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) a)
ho₂ : 2 < (fun x ↦ ω ^ x) a
⊢ (fun x ↦ ω ^ x) a ≤ 2 ∨ (fun x ↦ ω ^ x) a ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi✝ : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
hi : i < o
⊢ (fun a ↦ preBeth ↑a) ⟨Ordinal.lift.{v, u_1} i, hi✝⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
exact ⟨⟨i, hi⟩, IH _ hi⟩

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

Goal state before:
pp: a✝¹ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝¹ : Ordinal.{?u.6}
a✝ o✝ : Ordinal.{u}
f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o

Tactic:
rw [← hg.2.2]; apply lt_blsub

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, (f i).ord < a.ord

Tactic:
apply Ordinal.iSup_lt_of_lt_cof

Goal state after:
case ha
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ #α < a.ord.cof

case hf
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ∀ (i : α), (f i).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ 0)

Tactic:
omega_zero

Goal state after:
case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) ω
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (o.blsub fun b hb ↦ f (g b hb)) = f a

Tactic:
rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]

Goal state after:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun b x ↦ f b) = f a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
⊢ ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = (type r).cof

Tactic:
by
  classical
  let := linearOrderOfSTO r
  have : WellFoundedLT α := H.toIsWellFounded
  have : NoMaxOrder α := isSuccPrelimit_type_lt_iff.1 h.isSuccPrelimit
  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
  refine ⟨s, ?_, hs'⟩
  rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs

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

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ ℵ₀ = max ℵ₀ #α

Tactic:
eq_comm,

Goal state after:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ max ℵ₀ #α = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #α = max ℵ₀ #α

Tactic:
eq_comm,

Goal state after:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ max ℵ₀ #α = #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty (Quotient.out x)
| max ℵ₀ #(Quotient.out x)

Tactic:
mk_out

Goal state after:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty (Quotient.out x)
| max ℵ₀ x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
⊢ (single i (x i)).piecewise (erase i x) {i} = x

Tactic:
by
  ext j; rw [piecewise_apply]; split_ifs with h
  · rw [(id h : j = i), single_eq_same]
  · exact erase_ne h

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (single i b + erase i f) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Goal state after:
case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (single i b + erase i f) i

case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (single i b + erase i f) j
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain h hh (r • f) = r • comapDomain h hh f

Tactic:
ext
  rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (erase i f + single i b) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Goal state after:
case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (erase i f + single i b) i

case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (erase i f + single i b) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : ¬i = j
⊢ (f + single i b) j = (single i b + f) j

Tactic:
simp [H]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator

Tactic:
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
constructor <;> rintro ⟨μ, hμ⟩

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∃ f, (f.sum fun x xi ↦ ↑xi) = a
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 0

Tactic:
simp +contextual [hg0]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
simp_rw [iSupIndep_def, Submodule.disjoint_def]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))

Tactic:
congr! 1

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + (r₂ • x + l₂.eval) = r₂ • x + (l₁.eval + l₂.eval)
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x + l₂.eval = r₂ • x + l₁.eval + l₂.eval

Tactic:
congr! 1

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x = r₂ • x + l₁.eval
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))

Tactic:
congr! 1

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval

Tactic:
congr! 1

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval

Tactic:
congr! 1

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
hf : f i = 0
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
grind [Finsupp.sum, Finset.sum_congr]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
⊢ ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I

Tactic:
simp [hJ]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
x : M
hx : f x = 0
this : x ∈ span R (Set.range v)
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
c : ι →₀ R
hx : f (c.sum fun i a ↦ a • v i) = 0
this : (c.sum fun i a ↦ a • v i) ∈ span R (Set.range v)
⊢ (c.sum fun i a ↦ a • v i) = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : Monoid M
ψ : AddChar A M
⊢ ⇑ψ = 1 ↔ ψ = 0

Tactic:
by rw [← coe_zero, DFunLike.coe_fn_eq]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ 1 = a

Tactic:
eq_comm,

Goal state after:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ a = 1