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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ sSup (o.brange f) = o.bsup f

Tactic:
congr

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ o.brange f = range (o.familyOfBFamily f)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ a = (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

Tactic:
rw [← enum_typein (α := ToType 1) (· < ·) a]

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a, ⋯⟩ =
    (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a, ⋯⟩ =
    (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

Tactic:
congr

Goal state after:
case e_6
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ log b n = 0

Tactic:
log,

Goal state after:
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ (if b ≤ 1 then 0 else (log.go n b n).snd) = 0
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
have := @lsub_pos.{_, v} _ ⟨i⟩ f

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
by
  obtain rfl | hb := eq_or_ne b 0
  · simp
  · rw [mul_add_one, lt_add_iff hb]

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

Goal state before:
pp: o : Ordinal.{u_3}
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = sSup (Iic o)

Tactic:
congr

Goal state after:
o : Ordinal.{u_3}
⊢ (fun b ↦ b < (typein fun x1 x2 ↦ x1 < x2).top) = fun x ↦ x ≤ o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ log b y < x ↔ y < b ^ x

Tactic:
log,

Goal state after:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ (if b ≤ 1 then 0 else (log.go y b y).snd) < x ↔ y < b ^ x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
⊢ a / b = c

Tactic:
by
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp at hlt
  exact le_antisymm (div_le hb |>.mpr hlt) (mul_le_iff_le_div hb |>.mp hle)

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * (d - b)

Tactic:
rw [mul_sub, ← e, add_sub_cancel]

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

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n : ℕ
IH : a ^ ↑n = a ^ n
⊢ a ^ ↑(n + 1) = a ^ (n + 1)

Tactic:
rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]

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

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

Tactic:
by rw [opow_add, opow_one]

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

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

Tactic:
log,

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup ((fun x ↦ 1 ^ x) ⁻¹' Iic x) = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_of_left_le_one hb]

Goal state after:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, ∀ x_1 ∈ s, x < x_1 → ∀ x_2 ∈ s, b < x_2 → ∃ b_1 ∈ s, op x b < b_1

Tactic:
y

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y : Ordinal.{u_1}
⊢ ∀ x_1 ∈ s, x < x_1 → ∀ x_2 ∈ s, y < x_2 → ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * b = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, x < o → b < o → (fun x1 x2 ↦ x1 + x2) x b < o

Tactic:
y

Goal state after:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
⊢ x < o → y < o → (fun x1 x2 ↦ x1 + x2) x y < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: γ : Type u
inst✝ : LinearOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = Order.cof γ

Tactic:
by
  simpa using lift_cof_iSup_add_one hf

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

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ b = c

Tactic:
rw [lt_aleph0] at *

Goal state after:
case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ sSup (range fun i ↦ f i + 1) < a

Tactic:
range_comp' (· + 1)

Goal state after:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ sSup ((fun x ↦ x + 1) '' range f) < a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord

Tactic:
cof_zero,

Goal state after:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ ord 0
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl.inr
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)

Tactic:
· exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [← mk_toType o]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.ToType
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ω_ o).cof = ℵ_ o

Tactic:
rw [← ord_aleph, H.cof_ord]

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
⊢ (a * b).cof = b.cof

Tactic:
by_cases hb' : IsMin b
  · simp [hb'.eq_bot]
  · exact cof_map_of_isNormal (isNormal_mul_right ha.pos) ⟨hb', hb⟩

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ (sum fun n ↦ x ^ n) = max ℵ₀ x

Tactic:
have := nonempty_out h
  conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]

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

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x

Tactic:
congr

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ ↑(Classical.choose this) = x
Module: Mathlib.Data.DFinsupp.Ext

Goal state before:
pp: case h0
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

pp: case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
· exact AddSubmonoid.zero_mem _

Goal state after:
case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
Module: Mathlib.Data.DFinsupp.Submonoid

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

Tactic:
y

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
x✝¹ x✝ : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁✝ s₁ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
⊢ { toFun := f₁, support' := s₁✝ } = { toFun := f₁, support' := s₁ }

Tactic:
congr

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
x✝¹ x✝ : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁✝ s₁ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
⊢ s₁✝ = s₁
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ↑↑s) → β ↑i
⊢ ∀ ⦃a₂ : (i : ↑↑s) → β ↑i⦄, mk s x = mk s a₂ → x = a₂

Tactic:
y

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
⊢ mk s x = mk s y → x = y
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ x✝ ∈ f.dualMap.ker ↔ x✝ ∈ f.range.dualAnnihilator

Tactic:
simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]

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

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ LinearIndepOn R v t

Tactic:
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
⊢ AddMonoidHom.mrange (mapRange.addMonoidHom f) =
    AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i))

Tactic:
by
  classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]

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
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
⊢ p i ≤ ((lsum ℕ) fun i ↦ (p i).subtype).range

Tactic:
y

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
⊢ y ∈ p i → y ∈ ((lsum ℕ) fun i ↦ (p i).subtype).range
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
rw [LinearIndependent, this]

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R))
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
this : ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
LinearMap.ker_eq_bot

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
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
x✝ y x : M
⊢ ∀ (y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
y

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
⊢ (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ (map ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (-x.1, x.2)) l).sum = (map ((fun x ↦ -x) ∘ fun x ↦ x.1 • x.2) l).sum

Tactic:
congr

Goal state after:
case e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (-x.1, x.2)) = (fun x ↦ -x) ∘ fun x ↦ x.1 • x.2
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x ↦
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (r * x.1, x.2)) l).sum = (map ((fun x ↦ r • x) ∘ fun x ↦ x.1 • x.2) l).sum

Tactic:
congr

Goal state after:
case e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x ↦
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (r * x.1, x.2)) = (fun x ↦ r • x) ∘ fun x ↦ x.1 • x.2
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (map ((fun x ↦ x.1 • x.2) ∘ fun x ↦ ((Algebra.algebraMap S R) x.1, x.2)) l).sum = (map (fun x ↦ x.1 • x.2) l).sum

Tactic:
congr

Goal state after:
case e_f
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ ((Algebra.algebraMap S R) x.1, x.2)) = fun x ↦ x.1 • x.2
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := ⋯
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) a = ((lsum ℕ) fun i ↦ (p i).subtype) 0

Tactic:
← lsum_comp_mapRange_toSpanSingleton _ hv

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl :
  (((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
        (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R))
      l =
    0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) a = ((lsum ℕ) fun i ↦ (p i).subtype) 0
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
x✝ y x : M
⊢ ∀ (y : M), (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
y

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
⊢ (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case mk.mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
toFun✝¹ : A → M
map_zero_eq_one'✝¹ : toFun✝¹ 0 = 1
map_add_eq_mul'✝¹ : ∀ (a b : A), toFun✝¹ (a + b) = toFun✝¹ a * toFun✝¹ b
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h :
  { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ }.toFun =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ } =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }

Tactic:
congr

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∏ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
rw [coe_prod, Finset.prod_apply]

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (s ∪ {x})

Tactic:
have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ LinearIndepOn K v (s ∪ {x})
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
⊢ ∀ y ∈ span R (range v), c • x + y = 0 → c = 0

Tactic:
y

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
⊢ y ∈ span R (range v) → c • x + y = 0 → c = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ ((algebraMap R K) c)⁻¹ • -y ∈ span K (range v)

Tactic:
smul_neg

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ -(((algebraMap R K) c)⁻¹ • y) ∈ span K (range v)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ span K (range (v ∘ Subtype.val)) = span K t

Tactic:
congr

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ range (v ∘ Subtype.val) = t