mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ cof α < ℵ₀ ↔ cof α ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩
  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
  have hf : s.Finite := by
    rw [Set.Finite, ← mk_lt_aleph0_iff]
    exact hs'.trans_lt h
  obtain ⟨t, ht, ht'⟩ := hf.exists_subsingleton_isCofinal hs
  apply (cof_le ht').trans
  simpa

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a • b < 0

Tactic:
obtain ha | rfl | ha := lt_trichotomy 0 a

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a • b < 0

case inr.inl
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
b : β
hab : 0 ≤ 0 • b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 • b < 0

case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a • b < 0
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∩ t)

Tactic:
by
  rw [← dirSupClosedOn_compl, compl_inter]; exact hs.compl.union hDL ht.compl

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{v, u + 1} (typeLT Ordinal.{u})

Tactic:
← lift_umax

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r a ((enum r) ⟨0, h0⟩)

Tactic:
rw [← enum_typein r a, enum_le_enum r]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ⟨0, h0⟩ ≤ ⟨(typein r).toRelEmbedding a, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
← lift_umax

Goal state after:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ a * b

Tactic:
convert! mul_le_mul_right (one_le_iff_pos.2 hb) a

Goal state after:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a * 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ GaloisConnection ord card

Tactic:
by
  refine fun c o ↦ c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_
  let ⟨r, _, e⟩ := exists_ord_eq α
  constructor <;> intro h
  · rw [e] at h
    exact card_le_card h
  · obtain ⟨f⟩ := h
    have g := RelEmbedding.preimage f s
    have := RelEmbedding.isWellOrder g
    exact (ord_le_type _).trans g.ordinal_type_le

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

Goal state before:
pp: case zero
⊢ ↑0 ≤ (↑0).ord

Tactic:
exact zero_le

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

Goal state before:
pp: n : ℕ
⊢ n.log2 = log 2 n

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · rw [log2_zero, log_zero_right]
  apply eq_of_forall_le_iff
  intro m
  rw [Nat.le_log2 hn, Nat.le_log_iff_pow_le Nat.one_lt_two hn]

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

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b

Tactic:
exact zero_le

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + 1 = c

Tactic:
rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]
  rwa [← ord_aleph0, ord_le_ord]

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

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

Tactic:
derivFamily_succ,

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < nfpFamily f (succ (derivFamily f o))
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit.inl
ι : 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}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ o, derivFamily f o = a

Tactic:
exact ⟨_, h.symm⟩

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

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

Tactic:
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.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 ≤ o

Tactic:
exact zero_le

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

Goal state before:
pp: ⊢ ω < ω_ 1

Tactic:
rw [← omega_zero, omega_lt_omega]

Goal state after:
⊢ 0 < 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
rw [← isSuccPrelimit_type_lt_iff, ← hα]

Goal state after:
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥

Tactic:
rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ ∃ s, IsCofinal s ∧ typeLT ↑s = (Order.cof α).ord

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
⊢ ∃ s, IsCofinal s ∧ typeLT ↑s = (Order.cof α).ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < ⨆ a, 2 ^ preBeth ↑a

Tactic:
rw [lt_ciSup_iff' bddAbove_of_small]

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ i, preBeth a < 2 ^ preBeth ↑i
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
obtain ⟨x, xb, ax⟩ :=
        (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h

Goal state after:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b

Tactic:
opow_log_le_self b ha

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ a * b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
i : ι
hi : 1 < f i
⊢ ⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c

Tactic:
exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
⊢ (lsub f).cof ≤ #ι

Tactic:
exact cof_iSup_add_one_le f

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}
H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H

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

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ (↑(f i) + 1).card ≤ c

Tactic:
rw [card_le_iff]

Goal state after:
case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ ↑(f i) + 1 < (succ c).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Goal state after:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
⊢ ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = (type r).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} = 0 ↔ lift.{v, u} #α < lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0

Tactic:
by
  contrapose! +distrib
  rw [lift_mk_le', and_comm]
  simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_ofPred, exists_surjective_iff, nonempty_fun]

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

Goal state before:
pp: α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
rw [← isSuccPrelimit_type_lt_iff, ← hα]

Goal state after:
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) (single i ⟨y, hy⟩)) = y

Tactic:
filterAddMonoidHom_apply,

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) (filter p (single i ⟨y, hy⟩)) = y
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
⊢ f.sigmaUncurry.sigmaCurry = f

Tactic:
ext i j
    rw [sigmaCurry_apply, sigmaUncurry_apply]

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

Goal state before:
pp: case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
⊢ (sumZeroHom (Pi.single i φ)) { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } =
    (φ.comp { toFun := fun x ↦ x i, map_zero' := ⋯ }) { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ }

Tactic:
simp only [sumZeroHom, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk', ZeroHom.coe_comp,
    Function.comp_apply]

Goal state after:
case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
⊢ ∑ x ∈ sf.toFinset, (Pi.single i φ x) (f x) = φ (f i)
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
U V : Submodule R M
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
le_dualAnnihilator_iff_le_dualCoannihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ (U.dualAnnihilator ⊔ V.dualAnnihilator).dualCoannihilator
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).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

Tactic:
le_dualAnnihilator_iff_le_dualCoannihilator,

Goal state after:
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 ≤ (⨆ i, (U i).dualAnnihilator).dualCoannihilator
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f

Tactic:
apply DFinsupp.induction f

Goal state after:
case h0
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • 0) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) 0

case ha
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ ∀ (i : ι) (b : M i) (f : Π₀ (i : ι), M i),
    f i = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single i b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single i b + f)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ t = 0

Tactic:
by
  suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩
  exact h.eq_of_pair (by simpa using h')

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ g = 0

Tactic:
simpa using! hgsupp

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Surjective ⇑(Finsupp.linearCombination R v)

Tactic:
rwa [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
by
  simp only [eval_cons, ← h, add_assoc]

Goal state after:
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
⊢ (-l).eval = -l.eval

Tactic:
by
  simp +instances only [NF.eval, List.map_map, List.sum_neg, NF.instNeg]
  congr
  ext p
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)

Tactic:
rw [map_sup, mkQ_map_self, bot_sup_eq]

Goal state after:
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
⊢ LinearIndependent R v

Tactic:
by
  classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa

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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))

Tactic:
rw [hxy]

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f y₁ y₂ ∈ span R (range (f y₁))
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ.mulShift ↑n) x = ψ x ^ n

Tactic:
by
  rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
f : M → N
g : N → O
x✝ : S[M]
a✝ : O
⊢ ((mapDomainLinearMap R S (g ∘ f)) x✝).coeff a✝ = ((mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f) x✝).coeff a✝

Tactic:
simp [Finsupp.mapDomain_comp]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun b ↦ f a b) t ⊆ u

Tactic:
image₂_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ a ∈ s, image (fun b ↦ f a b) t ⊆ u
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun a ↦ f a b) s ⊆ u

Tactic:
image₂_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, image (fun a ↦ f a b) s ⊆ u
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g₁ s) (image g₂ t))

Tactic:
push_cast
    exact image_image2_distrib h_distrib

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
f : N →ₙ* O
g : M →ₙ* N
x✝ : R[M]
a✝ : O
⊢ ((mapDomainNonUnitalRingHom R (f.comp g)) x✝).coeff a✝ =
    (((mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)) x✝).coeff a✝

Tactic:
simp [Finsupp.mapDomain_comp]

Goal state after: