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

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #↑s

Tactic:
apply cof_le

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
s : Set α
hs : Unbounded r s
⊢ IsCofinal s
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
cases h

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ c.ord.cof < c

Tactic:
← not_le

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof

Tactic:
tauto

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

Goal state before:
pp: c : Cardinal.{u_1}
this : ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
← not_le

Goal state after:
c : Cardinal.{u_1}
this : ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
this : ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #α = #↑tᶜ

Tactic:
mk_compl_of_infinite t ht

Goal state after:
α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #α = #α
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : ⟨i, xi⟩ = ⟨j, xj⟩
⊢ single i xi = single j xj

Tactic:
cases h

Goal state after:
case refl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = single i xi
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : i✝ = i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x

Tactic:
cases h

Goal state after:
case pos.refl
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i : ι
c : γ
x : β i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update i 0 = erase i f

Tactic:
by
  ext j
  rcases eq_or_ne i j with (rfl | hi)
  · simp
  · simp [hi.symm]

Goal state after:
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:
by
  ext
  rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

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

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ (single i (single j x)).sigmaUncurry ⟨i', j'⟩ = (single ⟨i, j⟩ x) ⟨i', j'⟩

Tactic:
rw [sigmaUncurry_apply]

Goal state after:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ ∑ i_1 ∈ {i}.toFinset, (φ i_1) (Pi.single i x i_1) = (φ i) x

Tactic:
rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]

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

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

Tactic:
rw [extendWith_none]

Goal state after:
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 ∈ (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
simp [LinearMap.ext_iff (f := dualMap f x)]

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

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨by simpa using congr($h 0), by simpa using congr($h 1)⟩

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 : LinearIndependent R v
x✝¹ : ι
x✝ : M
⊢ x✝ ∈ R ∙ v x✝¹ ↔ x✝ ∈ Submodule.map (Finsupp.linearCombination R v) (Finsupp.lsingle x✝¹).range

Tactic:
simp [mem_span_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : 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
x : ι
hx : x ∉ s
⊢ ↑(μ x) ∈ ⊥

Tactic:
suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)

Goal state after:
case h.h
ι : 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
x : ι
hx : x ∉ s
⊢ ⊥ = ⨆ (_ : x ∈ s), p x
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : 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
x : ι
hx : x ∉ s
⊢ ⊥ = ⨆ (_ : x ∈ s), p x

Tactic:
exact (iSup_neg hx).symm

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
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
tauto

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✝ h : S ≤ T
⊢ map S.mkQ T ≤ (S.mapQ T LinearMap.id h).ker

Tactic:
by
      rintro _ ⟨x, hx, rfl⟩
      rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
      exact (Quotient.mk_eq_zero _).mpr hx

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ (a • f) x✝ = ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝

Tactic:
simp [Algebra.smul_def]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
t : R
v : ι → R
x✝ : ι
⊢ (⇑(algebraMap R A) ∘ (t • v)) x✝ = ((RingHom.id R) t • ⇑(algebraMap R A) ∘ v) x✝

Tactic:
simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
⊢ (of x).support = {x}

Tactic:
by
  rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]

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
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s = 0
h₂ : t = 0
⊢ s = 0 ∧ t = 0

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
rw [Finset.sum_comp]

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun g ↦ g i) (piFinset fun x ↦ s), #({a ∈ piFinset fun x ↦ s | a i = b}) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b
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)
hsp : span R (Set.range (⇑f ∘ v)) = ⊤
⊢ Bijective ⇑f

Tactic:
by
  refine ⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩
  rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp
  rwa [← range_eq_top]

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn K id {x, y}

Tactic:
by
  rw [pair_comm]; exact .id_insert (.singleton hx) <| by simpa [mem_span_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ a ∈ (List.replicate n s).prod

Tactic:
List.prod_replicate

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ a ∈ s ^ n
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝ : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t✝)
t s' : Finset V
hs' : ↑s' ⊆ s
x✝ : s ∩ ↑∅ = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ ∅))
this : s = ↑s'
⊢ ↑s' ⊆ s ∪ ↑∅ ∧ s ⊆ ↑s' ∧ s'.card = (s' ∪ ∅).card

Tactic:
simp [this]

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : u.card = (insert b₂ s' ∪ t).card
⊢ u.card = (s' ∪ insert b₁ t).card

Tactic:
by simp [eq, hb₂t', hb₁t, hb₁s']

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0

Tactic:
simp_rw [coeff_mul, sum, ← Finset.sum_product']
  refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]
  · refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
    exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]
  · refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
    rcases not_and_or.mp hnotMem with af | bg
    · rw [notMem_support_iff.mp af, zero_mul]
    · rw [notMem_support_iff.mp bg, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
← toFinsupp_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = toFinsupp 0 ↔ a = 0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

Tactic:
cases h

Goal state after:
case pos.refl
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x y : φ i
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨i, y⟩ = (single ⟨i, x⟩ 1) ⟨i, y⟩
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
⊢ (l.sum fun a m ↦ m • id (g a)) ∈ s

Tactic:
refine s.sum_mem ?_

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
⊢ ∀ c ∈ l.support, (fun a m ↦ m • id (g a)) c (l c) ∈ s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left.h_add
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
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
· exact fun _ _ _ => add_smul _ _ _

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

Goal state before:
pp: case a.refine_2.right.h_add
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
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
· exact fun _ _ _ => add_smul _ _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ (f.prod g).range = ⊤

Tactic:
simp [range_prod_eq hfg.sup_eq_top, *]

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

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]
  exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem.mem
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ x ∈ t, (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.mem.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.mem.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.mem.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
· intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩

Goal state after:
case a.mem.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ ((singleton r x).append p hx).append q ⋯ = (singleton r x).append (p.append q hq) ⋯

Tactic:
append_assoc

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ (singleton r x).append (p.append q ?hqw) ⋯ = (singleton r x).append (p.append q hq) ⋯

case hqw
α : Type u_1
r : SetRel α α
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ (p.last, q.head) ∈ r
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
this : ⊤ ≤ height b
⊢ ⊤ + 1 ≤ height b

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
this : ⊤ ≤ coheight b
⊢ ⊤ + 1 ≤ coheight b

Tactic:
simp [this]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁵ : CommSemiring R
inst✝³⁴ : CommSemiring R₂
inst✝³³ : CommSemiring R₃
inst✝³² : Monoid R'
inst✝³¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid N
inst✝²⁸ : AddCommMonoid P
inst✝²⁷ : AddCommMonoid Q
inst✝²⁶ : AddCommMonoid S
inst✝²⁵ : AddCommMonoid P'
inst✝²⁴ : AddCommMonoid Q'
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P₂
inst✝²⁰ : AddCommMonoid Q₂
inst✝¹⁹ : AddCommMonoid M₃
inst✝¹⁸ : AddCommMonoid N₃
inst✝¹⁷ : AddCommMonoid P₃
inst✝¹⁶ : AddCommMonoid Q₃
inst✝¹⁵ : DistribMulAction R' M
inst✝¹⁴ : Module R'' M
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Module R S
inst✝¹⁰ : Module R P'
inst✝⁹ : Module R Q'
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₂ N₂
inst✝⁶ : Module R₂ P₂
inst✝⁵ : Module R₂ Q₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₃ N₃
inst✝² : Module R₃ P₃
inst✝¹ : Module R₃ Q₃
inst✝ : Subsingleton M
z : M ⊗[R] N
⊢ 0 + 0 = 0

Tactic:
apply add_zero

Goal state after: