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

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ b ^ log b x ≤ x

Tactic:
rw [← one_le_iff_ne_zero] at hx
    obtain rfl | rfl := le_one_iff.1 hb <;> simpa

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ a + a < ω ^ o

Tactic:
apply (add_lt_add_of_le_of_lt hm.le hm).trans_le

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑m + ω ^ c * ↑m ≤ ω ^ o
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
omega_lt_omega

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

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))

Tactic:
← Cardinal.lift_umax,

Goal state after:
case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{max u v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.card ≤ ℵ₀

Tactic:
rwa [card_le_iff, succ_aleph0, ord_aleph]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
⊢ ¬(⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩ ∨ r ⟨↑y, ⋯⟩ ⟨↑x, ⋯⟩)

Tactic:
rintro (_ | hxy')

Goal state after:
case refine_2.inl
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
h✝ : ⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩
⊢ False

case refine_2.inr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
hxy' : r ⟨↑y, ⋯⟩ ⟨↑x, ⋯⟩
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ a * b < ω ^ succ c

Tactic:
an,

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * n * b < ω ^ succ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b

Tactic:
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < preBeth o
⊢ 2 ^ x < preBeth o

Tactic:
rw [preBeth_limit ho] at hx

Goal state after:
case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
⊢ 2 ^ x < preBeth o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)

Tactic:
lift_preBeth,

Goal state after:
o : Ordinal.{u_1}
⊢ preBeth (Ordinal.lift.{v, u_1} (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
simpa using lift_iSup_add_one_lt_of_lt_cof ha hf

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

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ ⨆ i, f i * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
Cardinal.mul_ciSup g

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

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬(a ^ b).card = 0

Tactic:
card_eq_zero,

Goal state after:
case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬a ^ b = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(List α) = max #α ℵ₀

Tactic:
rw [mk_list_eq_max, max_comm]

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

Goal state before:
pp: case inl
α : Type u
h✝ : Finite α
⊢ #(List α) ≤ max ℵ₀ #α

pp: case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
· exact mk_le_aleph0.trans (le_max_left _ _)

Goal state after:
case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
⊢ Finite ι

Tactic:
have := congr(($hsspan).map b.repr.toLinearMap)

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : Submodule.map (↑b.repr) (span R s) = Submodule.map ↑b.repr ⊤
⊢ Finite ι
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
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
⊢ #ι ≤ #↑(range Φ)

Tactic:
apply Cardinal.le_range_of_union_finset_eq_univ

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
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := ⋯
⊢ ⋃ a, ↑(Φ a) = Set.univ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ (if i ≠ j then single i x else 0) = if i = j then 0 else single i x

Tactic:
ite_not

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ (if i = j then 0 else single i x) = if i = j then 0 else single i x
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMulZeroClass γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
⊢ filter p (r • f) = r • filter p f

Tactic:
by
  ext
  simp [smul_apply, smul_ite]

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 : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ ij.fst ij.snd
⊢ (single ij x).sigmaCurry = single ij.fst (single ij.snd x)

Tactic:
obtain ⟨i, j⟩ := ij

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ (single i m).toDFinsupp = DFinsupp.single i m

Tactic:
by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ (single i m).toFinsupp = Finsupp.single i m

Tactic:
by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ (erase i f).support

Tactic:
subst hb
    simp [update_eq_erase, support_erase]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain h hh (single (h k) x)) i = (single k x) i

Tactic:
rw [comapDomain_apply]

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: 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

Tactic:
smul_zero,

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) 0 = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ m ∈ ⨆ i, (lsingle i).range

Tactic:
rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]

Goal state after:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ ((lsum ℕ) lsingle) m ∈ ⨆ i, (lsingle i).range
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support

Tactic:
ext x
  simp [h]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + r • l' i • m = r • 0
⊢ l' = 0

Tactic:
smul_zero,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + r • l' i • m = 0
⊢ l' = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
has : a ∈ s
⊢ f a ∈ span K (f '' s) ↔ LinearIndepOn K f (insert a s) → a ∈ s

pp: case neg
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
has : a ∉ s
⊢ f a ∈ span K (f '' s) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
· exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has

Goal state after:
case neg
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
has : a ∉ s
⊢ f a ∈ span K (f '' s) ↔ LinearIndepOn K f (insert a s) → a ∈ s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

Tactic:
by_contra hc

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ ↑(image₂ f s (t ∩ t')) = ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast
    exact image2_inter_right hf

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ MonoidAlgebra.opRingEquiv.symm (single x r) = op (single (unop x) (unop r))

Tactic:
by
  apply MulOpposite.unop_injective; ext; simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ single m a = single n b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
single_inj

Goal state after:
R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ m = n ∧ a = b ∨ a = 0 ∧ b = 0 ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = q • C 1 * f

Tactic:
C_1,

Goal state after:
R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = q • 1 * f
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = a • C 1 * f

Tactic:
C_1,

Goal state after:
R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = a • 1 * f
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
inst✝ : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ ∀ (i : ι), LinearIndependent R fun x ↦ v i

Tactic:
simp +contextual [hv]

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

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))

Goal state after:
case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : ai ∈ image (fun x ↦ x i) A
bi : G i
hB : bi ∈ image (fun x ↦ x i) B
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : IsDomain R
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ ∀ (i : ι), LinearIndependent R fun x ↦ v i

Tactic:
simp +contextual [hv]

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

Goal state before:
pp: 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
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
⊢ s.FG

Tactic:
have := Classical.decEq R

Goal state after:
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
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
this : DecidableEq R
⊢ s.FG
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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]

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
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 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2

Tactic:
Prod.fst_add,

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 + ψ.1) (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

Tactic:
rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r
length_eq : { length := nx, toFun := fx, step := step✝ }.length = y.length
toFun_eq : { length := nx, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y

Tactic:
dsimp only at length_eq

Goal state after:
α : Type u_1
r : SetRel α α
y : RelSeries r
nx : ℕ
fx : Fin (nx + 1) → α
step✝ : ∀ (i : Fin nx), (fx i.castSucc, fx i.succ) ∈ r
length_eq : nx = y.length
toFun_eq : { length := nx, toFun := fx, step := step✝ }.toFun = y.toFun ∘ Fin.cast ⋯
⊢ { length := nx, toFun := fx, step := step✝ } = y
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
| p.length + 1 + (↑i - p.length)

Tactic:
Nat.add_comm p.length 1,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
| 1 + p.length + (↑i - p.length)
Module: Mathlib.Order.KrullDimension

Goal state before:
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:
· simpa [hfin, ENat.lt_add_one_iff] using height_le_coe_iff (x := x) (n := n + 1)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b

Tactic:
exact forall_comm

Goal state after: