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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) = ⨆ i, List.foldr f a i

Tactic:
apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_

Goal state after:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)

Tactic:
Nat.add_sub_cancel,

Goal state after:
case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c < n ↔ c * k < clog b n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
rw [derivFamily_limit _ l, H.map_iSup bddAbove_of_small]

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ sInf {x | x.IsInitial} = 0

Tactic:
exact csInf_eq_bot_of_bot_mem isInitial_zero

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

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

Tactic:
nfp_mul_zero,

Goal state after:
case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ 0 = a ^ ω * 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 < o.cof ↔ IsSuccLimit o

Tactic:
← not_iff_not,

Goal state after:
o : Ordinal.{u_1}
⊢ ¬1 < o.cof ↔ ¬IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
apply this

Goal state after:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
conv_lhs => rw [← one_mul (ω ^ _)]
      grw [one_le_iff_pos.2 a0]

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

Goal state before:
pp: ⊢ ℶ_ 0 = ℵ₀

Tactic:
simp [beth]

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

Goal state before:
pp: case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀

pp: case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
· rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _

Goal state after:
case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a + b < ℵ₀
⊢ b = 0

Tactic:
add_lt_aleph0_iff,

Goal state after:
case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀ ∧ b < ℵ₀
⊢ b = 0
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Function.Surjective fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
⊢ ∃ a, (fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩) a = ⟨x, hx⟩
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

Tactic:
cases omega0_pos.not_ge ha

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = o.cof

Tactic:
cof_eq_sInf_lsub

Goal state after:
o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
cof_eq_sInf_lsub

Goal state after:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ #↑(f ⁻¹' {x}) ≤ #β

Tactic:
rw [le_mk_iff_exists_set]

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ ∃ p, #↑p = #↑(f ⁻¹' {x})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s // Bounded r s } = #α

Tactic:
have h' : IsStrongLimit #α := ⟨ha, @h⟩

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // Bounded r s } = #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } ≤ #α

Tactic:
have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := ofPred_exists _

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #{ s // Bounded r s } ≤ #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
have h' : IsStrongLimit #α := ⟨ha, @h⟩

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ Nonempty (α → β') ∧ Nonempty (β' ↪ α) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)

Tactic:
nonempty_fun

Goal state after:
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
⊢ IsCofinal s

Tactic:
IsCofinal,

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 α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, x ≤ y
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ nfpFamily f a < c.ord

Tactic:
apply nfpFamily_lt_ord_lift _ _ hf ha <;> rw [hc.cof_ord]
  · exact lt_of_le_of_ne hc.1 hc'.symm
  · exact hι

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

Goal state before:
pp: case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max (max (u + 1) (v + 1)) u v, max u v} b.card < lift.{max (u + 1) (v + 1), max u v} c

Tactic:
lift_lt,

Goal state after:
case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ b.card < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (ℵ_ ω).IsSingular

Tactic:
by simp [isSingular_aleph_iff]

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1 + 1, u_1} a.card < lift.{u_1 + 1, u_1} c

Tactic:
lift_lt,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ a.card < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ
h : α ≃ β := (Set.sumCompl s).symm.trans (((ofInjective ⇑f ⋯).sumCongr g).trans (Set.sumCompl (range ⇑f)))
⊢ ∀ (x : ↑s), h ↑x = f x

Tactic:
rintro ⟨x, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ
h : α ≃ β := (Set.sumCompl s).symm.trans (((ofInjective ⇑f ⋯).sumCongr g).trans (Set.sumCompl (range ⇑f)))
x : α
hx : x ∈ s
⊢ h ↑⟨x, hx⟩ = f ⟨x, hx⟩
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case pos
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

pp: case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
· simp [hp]

Goal state after:
case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
· simp [hp]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : (single i xi) i = (single j xj) i
hcj : (single i xi) j = (single j xj) j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
DFinsupp.single_eq_same

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = (single j xj) i
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (f g.fst) g.snd ≠ 0
⊢ g.fst ∈ f.support

Tactic:
simp only [Ne, DFinsupp.mem_support_toFun]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (f g.fst) g.snd ≠ 0
⊢ ¬f g.fst = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : 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)
⊢ (f.update i b).support = if b = 0 then (erase i f).support else insert i f.support

Tactic:
ext j
  split_ifs with hb
  · subst hb
    simp [update_eq_erase, support_erase]
  · rw [support_update_ne_zero f _ hb]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x

Tactic:
simp only [Forall, Fin.forall_fin_zero_pi]

Goal state after:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g

Tactic:
exact hfg

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
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
⊢ Bijective ⇑(eval R (Dual R M))

Tactic:
simpa only [← symm_dualMap_evalEquiv] using! (evalEquiv R M).dualMap.symm.bijective

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₂
⊢ f.dualMap.range ≤ f.ker.dualAnnihilator

Tactic:
rintro _ ⟨ψ, rfl⟩

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₂
ψ : Dual R M₂
⊢ f.dualMap ψ ∈ f.ker.dualAnnihilator
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

pp: case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
· simp [hp]

Goal state after:
case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
· simp [hp]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]

Goal state after:
ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨x, hx⟩ ∈ (subToSupQuotient p p').range
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
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (LinearMap.id x) = 0

Tactic:
exact (Quotient.mk_eq_zero _).mpr hx

Goal state after:
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]
  constructor
  · intro h s v w hvw
    simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2
  · 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
x : X
a : FreeAbelianGroup X
⊢ x ∉ a.support ↔ (coeff x) a = 0

Tactic:
by
  rw [support, Finsupp.notMem_support_iff]
  exact Iff.rfl

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

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

Tactic:
Finsupp.support_single _ one_ne_zero

Goal state after:
X : Type u_1
x : X
⊢ {x} = {x}
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ s 0 * (List.ofFn fun i ↦ s i.succ).prod ↔
    ∃ a_1 v, ↑(Fin.cons a_1 v 0) * (List.ofFn fun i ↦ ↑(Fin.cons a_1 v i.succ)).prod = a

Tactic:
Fin.cons_zero,

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ s 0 * (List.ofFn fun i ↦ s i.succ).prod ↔ ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(Fin.cons a_1 v i.succ)).prod = a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ ↑(image₂ f (image g s) t) = ↑(image₂ (fun a b ↦ f (g a) b) s t)

Tactic:
push_cast
    exact image2_image_left _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [sup'_le_iff, forall_mem_image₂]

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 t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ ht.toFinset.card

Tactic:
rw [← Eq]

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case inl
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : single (u i) 1 = (lmapDomain R R u) (single i 1)
⊢ single i 1 =
    (LinearMap.linearProjOfIsCompl (span R (Set.range fun x ↦ single (v x) 1)) (lmapDomain R R u) ⋯ ⋯) (single (u i) 1)

Tactic:
rw [this, LinearMap.linearProjOfIsCompl_apply_left]

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

Goal state before:
pp: case inl
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
⊢ (lcomapDomain u hu) (Finsupp.basisSingleOne (u i)) =
    (LinearMap.linearProjOfIsCompl (span R (Set.range fun x ↦ single (v x) 1)) (lmapDomain R R u) ⋯ ⋯)
      (Finsupp.basisSingleOne (u i))

Tactic:
have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
    simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
    rw [this, LinearMap.linearProjOfIsCompl_apply_left]

Goal state after: