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

Goal state before:
pp: α : Type u
β' : Type v
⊢ {f | Surjective f}.Nonempty ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)

Tactic:
Set.Nonempty,

Goal state after:
α : Type u
β' : Type v
⊢ (∃ x, x ∈ {f | Surjective f}) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ #↑{x} < (#α).ord.cof

case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α = lift.{v, u} #α + lift.{u, v} #β'

Tactic:
eq_comm

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := ⋯
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ LinearIndependent R v'

Tactic:
linearIndependent_iffₛ

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ ∀ (l₁ l₂ : Option κ →₀ R), (linearCombination R v') l₁ = (linearCombination R v') l₂ → l₁ = l₂
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
rw [DFinsupp.sumAddHom_apply]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (f.sum fun x ↦ ⇑(g x)) ∈ s
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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
⊢ { s // ∀ (i : ι), i ∈ s ∨ f i (x i) (y i) = 0 }

Tactic:
refine ⟨xs + ys, fun i => ?_⟩

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)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0} → i ∈ {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
intro H

Goal state after:
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | f i ≠ 0}
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0}
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0} → i ∈ {i ∈ sx.toFinset | f i ≠ 0}

Tactic:
intro H

Goal state after:
case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | f i ≠ 0}
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0}
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∈ ↑s
⊢ f i = 0 i

Tactic:
exact hs₁ _ hs₂

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ (sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ f.splitSupport

Tactic:
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm

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

Goal state before:
pp: case neg
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : ¬i = i'
⊢ (mapRange f hf (single i b)) i' = (single i (f i b)) i'

Tactic:
· simp [h, hf]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
⊢ comapDomain' ⇑h.symm ⋯ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f) = f

Tactic:
by
    ext k
    rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.apply_symm_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 : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ (↑⟨s, hf⟩).toFinset
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0 then
      (fun x ↦ ⇑(φ x)) i ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i)
    else 0

Tactic:
dsimp only [coe_mk', Subtype.coe_mk] at *

Goal state after:
case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ s.toFinset
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0 then
      (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i)
    else 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ ↑(sumAddHom (Pi.single i φ)) = ↑(φ.comp (evalAddMonoidHom i))

Tactic:
convert! sumZeroHom_piSingle i φ.toZeroHom using 1

Goal state after:
case e'_2
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ ↑(sumAddHom (Pi.single i φ)) = sumZeroHom (Pi.single i ↑φ)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: 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
a : ι
b : M a
f : Π₀ (i : ι), M i
a✝¹ : f a = 0
a✝ : b ≠ 0
hf : (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
    c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)

Tactic:
rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]

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

Goal state before:
pp: case inr
ι : 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
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
this : Std.Refl r
⊢ f = g

Tactic:
obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using! And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

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
⊢ ∀ (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

Tactic:
intro x y h s t

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
h : ∀ (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.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
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
add_comm,

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
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ t • x + s • y = 0 → s = 0 ∧ t = 0
Module: Mathlib.Tactic.Module

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

Tactic:
add_comm,

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

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ d • c • t + c • b • s = 0

Tactic:
add_comm,

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ c • b • s + d • c • t = 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 : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • (d • t + b • s) = 0

Tactic:
add_comm,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • (b • s + d • t) = 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 : M
⊢ LinearIndependent R ![y, x + y] ↔ LinearIndependent R ![x, y]

Tactic:
add_comm,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![y, y + x] ↔ LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case neg
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 : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Tactic:
have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)

Goal state after:
case neg
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 : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
h0 : f x₁ x₂ = 0
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ insert i (f.support.erase i), f i • v i = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
⊢ f i • v i ∈ span R (v '' I)

Tactic:
Finset.sum_insert (Finset.notMem_erase _ _),

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : f i • v i + ∑ x ∈ f.support.erase i, f x • v x = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
⊢ f i • v i ∈ span R (v '' I)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
⊢ Injective fun ψ ↦ f.compAddChar ψ

Tactic:
rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.comp_left h

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
s' : Submonoid (Multiplicative M) := Submonoid.closure s
h : of' R M m ∈ Submodule.span R ↑(Submonoid.map (of R M) s')
h' : Submonoid.map (of R M) s' = Submonoid.closure (⇑(of R M) '' s)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)

Tactic:
simpa using! of'_mem_span.1 h

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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

Tactic:
by_cases x ∈ s

Goal state after:
case pos
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∈ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t

case neg
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)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
x : V
h✝ : x ∉ s
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ ⇑({i}ᶜ.orderEmbOfFin h) = ⇑(RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb)

Tactic:
eq_comm

Goal state after:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ ⇑(RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) = ⇑({i}ᶜ.orderEmbOfFin h)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ a, (lapply a).ker ≤ ⊥

Tactic:
simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
  exact fun a h => Finsupp.ext h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = map (lsingle a) (span R s)

Tactic:
rw [← span_image]; rfl

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
⊢ ∀ (x : S₁) (y : S₂) (z : R[X]), (x • y) • z = x • y • z

Tactic:
rintro _ _ ⟨⟩
    simp_rw [← ofFinsupp_smul, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬a0 = a ∨ ¬b0 = b

Tactic:
eq_comm

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬a = a0 ∨ ¬b0 = b
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
by
  rw [sSup_eq_iSup, iSup_subtype', Submodule.mem_iSup_iff_exists_finset]
  refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype (· ∈ S)), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
  · simp
  · suffices m ∈ ⨆ (i) (hi : i ∈ S) (_ : ⟨i, hi⟩ ∈ s), i by simpa
    rwa [iSup_subtype']
  · have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert! rfl; grind
    simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]

Goal state after: