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

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
exact mul_eq_max h hb

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'.blsub g

Tactic:
apply lt_blsub

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

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

Tactic:
simp [hb]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ Function.update 0 i b i' = if h : i = i' then Eq.recOn h b else 0

Tactic:
Function.update

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ f.support → h x (f x) = 1

Tactic:
simp +contextual [h_zero]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ g.support → h x (g x) = 1

Tactic:
simp +contextual [h_zero]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ ∀ x ∈ f.support ∪ g.support, x ∉ (f + g).support → h x ((f + g) x) = 1

Tactic:
simp +contextual [h_zero]

Goal state after:
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) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ (Pi.single i φ i) (f i) = 0

Tactic:
simp [(hf i).resolve_left (by simpa using hi)]

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

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ extendWith x 0 = single none x

Tactic:
ext (_ | j)
  · rw [extendWith_none, single_eq_same]
  · rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]

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₂
hf : Function.Surjective ⇑f
φ : Dual R M₂
⊢ ∀ ⦃a₂ : Dual R M₂⦄, f.dualMap φ = f.dualMap a₂ → φ = a₂

Tactic:
ψ

Goal state after:
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₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
⊢ f.dualMap φ = f.dualMap ψ → φ = ψ
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
by
    let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
    have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) := by
      ext m f
      exact DFunLike.congr_arg f (e.apply_symm_apply m).symm
    simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
    exact Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)

Goal state after:
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
⊢ ∀ i ∈ t, g i = 0

Tactic:
have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]

Goal state after:
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}
⊢ ∀ i ∈ t, g i = 0
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 w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]

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
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) ↔
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
intro h s v hv hv0
    specialize h s v 0
    simp_all

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

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a = ∑ x ∈ a.support, (coeff x) a • of x

Tactic:
conv_lhs => rw [← toFreeAbelianGroup_toFinsupp a, ← sum_single a.toFinsupp]
  simp [sum, support, coeff]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
n : ℤ
ψ : AddChar A M
a : A
⊢ (n • ψ) a = ψ a ^ n

Tactic:
cases n <;> simp [-neg_apply, neg_apply']

Goal state after:
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
u : R
hu : IsUnit u
⊢ ψ.mulShift u = 1 ↔ ψ = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
⊢ ψ = 1

case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1
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
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ y = u * (↑hu.unit⁻¹ * y)

Tactic:
rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (a * a_1)) =
    (a.coeff.sum fun a b ↦ ↑f b * g a) * b.coeff.sum fun a b ↦ ↑f b * g a

Tactic:
Finsupp.sum_mul,

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (a * a_1)) =
    a.coeff.sum fun a c ↦ ↑f c * g a * b.coeff.sum fun a b ↦ ↑f b * g a
Module: Mathlib.Algebra.MonoidAlgebra.Lift

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (Multiplicative.ofAdd (a + a_1))) =
    (a.coeff.sum fun a b ↦ ↑f b * g (Multiplicative.ofAdd a)) * b.coeff.sum fun a b ↦ ↑f b * g (Multiplicative.ofAdd a)

Tactic:
Finsupp.sum_mul,

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (Multiplicative.ofAdd (a + a_1))) =
    a.coeff.sum fun a c ↦ ↑f c * g (Multiplicative.ofAdd a) * b.coeff.sum fun a b ↦ ↑f b * g (Multiplicative.ofAdd a)
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
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : SMulCommClass R S S
t : R
a b : S[M]
⊢ t • a • b = a • t • b

Tactic:
by
    classical ext; simp [coeff_mul, sum_smul_index', Finsupp.smul_sum, mul_smul_comm]

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 ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
← mem_prod_list_ofFn,

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ a ∈ (List.ofFn fun a ↦ s).prod
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 t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ ↑(span K (v '' b)) ∧ LinearIndepOn K v b

Tactic:
obtain ⟨b, sb, h⟩ := by
    refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
    · refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_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 t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun x ↦ x ∈ {b | b ⊆ t ∧ LinearIndepOn K v b}) b
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ ↑(span K (v '' b)) ∧ LinearIndepOn K v b
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : ¬∀ i ∈ s, Disjoint (image (f a) t) (image (f i) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
not_forall

Goal state after:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : ∃ x, ∃ (_ : x ∈ s), ¬Disjoint (image (f a) t) (image (f x) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun (x * y) =
      (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun x *
        (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun y

Tactic:
simp [coeff_mul, MonoidAlgebra.ext_iff, Finsupp.ext_iff, ← MulOpposite.unop_inj,
      unop_finsuppSum, sum_mapRange_index, apply_ite unop, mapAddEquiv]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (a a_1 : R[M]) (a_2 : M),
    (a_1.coeff.sum fun m₁ r₁ ↦ a.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = a_2 then r₁ * r₂ else 0) =
      a.coeff.sum fun i n ↦ a_1.coeff.sum fun i_1 n_1 ↦ if i_1 * i = a_2 then n_1 * n else 0
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u).range = span R (Set.range fun x ↦ single (u x) 1)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u).range ≤ span R (Set.range fun x ↦ single (u x) 1)

case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ span R (Set.range fun x ↦ single (u x) 1) ≤ (lmapDomain R R u).range
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Tactic:
simp_rw [← coe_inj]; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix ↦ single ix.fst (f ix.fst ix.snd)

Tactic:
classical
  convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ Pi.single s 1 * Pi.single x✝¹ 1 = 0

Tactic:
ext u

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
u : G
⊢ (Pi.single s 1 * Pi.single x✝¹ 1) u = 0 u
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ ∀ (y : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), ofIsCompl h (φ + y).1 (φ + y).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h y.1 y.2

Tactic:
ψ

Goal state after:
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ ψ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ ofIsCompl h (φ + ψ).1 (φ + ψ).2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝¹ a₁ a₂ : α
b✝ : β
c✝¹ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a✝ b c✝ a c : α
⊢ (a, c) ∈ R ○ R.inv → (c, a) ∈ R ○ R.inv

Tactic:
rintro ⟨b, hab, hbc⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝¹ a₁ a₂ : α
b✝¹ : β
c✝¹ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a✝ b✝ c✝ a c b : α
hab : (a, b) ∈ R
hbc : (b, c) ∈ R.inv
⊢ (c, a) ∈ R ○ R.inv
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ Nonempty α

Tactic:
by
  obtain ⟨p, _⟩ := (r.finiteDimensional_iff).mp ‹_›
  exact ⟨p 0⟩

Goal state after:
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
⊢ (p.cons x hx).append q ⋯ = (p.append q hq).cons x ⋯

Tactic:
simp only [cons]
  rw [append_assoc]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (p.tail len_pos).head = p.toFun 1

Tactic:
by
  change p (Fin.succ _) = p 1
  congr
  ext
  change (1 : ℕ) = (1 : ℕ) % _
  rw [Nat.mod_eq_of_lt]
  simpa only [lt_add_iff_pos_left, Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
n : ℕ
heq : p.length = n
⊢ motive p

Tactic:
by
    induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have ne0 : p.length ≠ 0 := by simp [heq]
      have len : p.eraseLast.length = d := by simp [heq]
      convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
      exact (p.snoc_self_eraseLast ne0).symm

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).last = p.last

Tactic:
by
  simp only [last, drop, Fin.last]
  congr
  lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lf, g⟩, mg⟩

Tactic:
Subtype.mk_eq_mk,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ ⟨lf, f⟩ = ⟨lf, g⟩
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_1
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ↔ ∃ y < x, height y = ↑n

pp: case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n

Tactic:
· exact coe_lt_height_iff hfin

Goal state after:
case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ 2 ≤ height x ↔ ∃ y, ∃ z < y, y < x

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
⊢ ∃ y, ∃ z < y, y < x

case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
i : Fin 1
⊢ (![x, y] i.castSucc, ![x, y] i.succ) ∈ {(a, b) | a < b}

Tactic:
obtain rfl := Subsingleton.elim i 0; simpa

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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
⊢ (SMul.aux r) (FreeAddMonoid.of (m, 0)) = (SMul.aux r) 0

Tactic:
simp_rw [map_zero, SMul.aux_of, tmul_zero]

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

Goal state before:
pp: case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m ↦ r • m)

Tactic:
obtain ⟨c, hc, rfl⟩ := h

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∃ c_1,
    ↑c_1.support ⊆ sR ∧ (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) c = ↑(c_1.sum fun r m ↦ r • m)