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

Goal state before:
pp: a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
by
    rw [← lift_umax]
    exact lift_type_le.{_, _, u}

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < b ^ (2 * fuel)

Tactic:
exact Nat.lt_of_lt_of_le hfuel <| Nat.pow_le_pow_right (by grind) (by grind)

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
by
  rw [← not_le, div_le h, not_lt]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)

Tactic:
rw [← card_eq_nat, card_type, mk_fintype]

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

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a

Tactic:
exact nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha

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

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

Tactic:
rw [← iSup_iterate_eq_nfp, ← iSup_pow_natCast ha]
  simp

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

Goal state before:
pp: ⊢ preOmega ω = ω

Tactic:
simp_rw [← apply_omega0_of_isNormal isNormal_preOmega, preOmega_natCast, iSup_natCast]

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

Goal state before:
pp: ⊢ range ⇑ω_ = {x | ω ≤ x ∧ x.IsInitial}

Tactic:
ext x
  constructor
  · rintro ⟨a, rfl⟩
    exact ⟨omega0_le_omega a, isInitial_omega a⟩
  · rintro ⟨ha', ha⟩
    obtain ⟨a, rfl⟩ := ha.mem_range_preOmega
    use a - ω
    rw [omega0_le_preOmega_iff] at ha'
    rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

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

Goal state before:
pp: case ind.mk.hbc.inl
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : #↑(Iio q) < ℵ₀
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
exact (mul_lt_aleph0 hq hq).trans_le hc

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ b < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Tactic:
lt_aleph0

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℶ_ o).IsStrongLimit ↔ IsSuccPrelimit o

Tactic:
rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]

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

Goal state before:
pp: case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ b < ℵ₀
⊢ b = 0

Tactic:
lt_aleph0

Goal state after:
case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
lt_aleph0

Goal state after:
case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x_1 ↦ o) i hi✝ < (fun x x_1 ↦ o) j hj✝

Tactic:
rw [hi, hj] at h

Goal state after:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x_1 ↦ o) i hi✝ < (fun x x_1 ↦ o) j hj✝
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) c.ord

Tactic:
apply (isInitial_ord c).isPrincipal_opow
  rwa [omega0_le_ord]

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

Goal state before:
pp: case refine_1
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ⊆ s

Tactic:
rintro x ⟨hx, _⟩
    exact hx

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
e : α ≃ α × Bool
this : 2 ^ #α ≤ #(Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f a)

Tactic:
← m

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)
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]

Goal state after:
ι : 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
⊢ ℵ₀ < c

ι : 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
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #α ^ #α = #(α → α)

Tactic:
power_def

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α → α) = #(α → α)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α)

Tactic:
by
    conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]
    obtain ⟨e⟩ := lift_mk_le'.mp lle
    exact ⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
      fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ (filter p f + filter (fun i ↦ ¬p i) f) i = f i

Tactic:
simp only [add_apply, filter_apply]; split_ifs <;> simp only [add_zero, zero_add]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
⊢ Quotient piSetoid

Tactic:
let e := Equiv.subtypeQuotientEquivQuotientSubtype (fun l : List ι ↦ ∀ i, i ∈ l)
    (fun s : Multiset ι ↦ ∀ i, i ∈ s) (fun i ↦ Iff.rfl) (fun _ _ ↦ Iff.rfl) ⟨_, Finset.mem_univ⟩

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ Quotient piSetoid
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 : ι
H : i ∈ {i ∈ sy.toFinset | f i ≠ 0}
left✝ : i ∈ sy.toFinset
h : f i ≠ 0
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0}

Tactic:
exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hx i).resolve_right h, h⟩

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (finHRecOn fun x ↦ ⟦a x⟧) = fun f x ↦ f a

Tactic:
ext f h
  refine eq_of_heq ((eqRec_heq _ _).trans ?_)
  rw [finChoice_eq]
  rfl

Goal state after:
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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : i ∉ f.support
hf : f i = 0
⊢ f i = g i

Tactic:
have hg : g i = 0 := by rwa [h₁, mem_support_iff, not_not] at h

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : i ∉ f.support
hf : f i = 0
hg : g i = 0
⊢ f i = g i
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')
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
by
  simp only [← Dual.eval_comp_comp_evalEquiv_eq]
  refine ⟨fun hfg => ?_, fun a ↦ congrArg (Dual.eval R M').comp
    (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩
  rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg
  exact hfg

Goal state after:
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
⊢ (F a).toAddMonoidHom (c • b) + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f =
    c • (F a).toAddMonoidHom b + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f

Tactic:
LinearMap.toAddMonoidHom_coe,

Goal state after:
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
⊢ (F a) (c • b) + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f =
    c • (F a) b + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, (f.sum fun x ↦ ⇑(p x).subtype.toAddMonoidHom) = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
LinearMap.toAddMonoidHom_coe,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, (f.sum fun x ↦ ⇑(p x).subtype) = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ψ x * ∑ a, ψ a = ∑ a, ψ a

Tactic:
rw [Finset.mul_sum]

Goal state after:
case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ i, ψ x * ψ i = ∑ a, ψ a
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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ Disjoint (span K (v '' s)) (K ∙ v x)

Tactic:
disjoint_span_singleton' x0

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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ v x ∉ span K (v '' s)
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
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, (lsingle a).range

Tactic:
exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ (C c * X ^ n).support = {n}

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, support_monomial n h]

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

Goal state before:
pp: 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
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
apply IsWellFounded.induction (· ⊂ ·) A

Goal state after:
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 := ⋯
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0) →
      ∀ {B : Finset ((i : ι) → G i)}, x.Nonempty → B.Nonempty → ∃ a0 ∈ x, ∃ b0 ∈ B, UniqueMul x B a0 b0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

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

Tactic:
have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ LinearIndependent R fun ix ↦ single ix.fst (f ix.fst ix.snd)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: 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 : ι), TwoUniqueProds (G i)
A : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
apply IsWellFounded.induction (· ⊂ ·) A

Goal state after:
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 : ι), TwoUniqueProds (G i)
A : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x,
        ∀ {B : Finset ((i : ι) → G i)},
          1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2) →
      ∀ {B : Finset ((i : ι) → G i)},
        1 < #x * #B → ∃ p1 ∈ x ×ˢ B, ∃ p2 ∈ x ×ˢ B, p1 ≠ p2 ∧ UniqueMul x B p1.1 p1.2 ∧ UniqueMul x B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : ⟨x, hpx⟩ = 0
⊢ x ∈ ⊥

Tactic:
mk_eq_zero

Goal state after:
case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x = 0
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R (g '' ↑t1) ⊔ span R ↑t2 ≤ s

Tactic:
refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ ↑t1 ⊆ g ⁻¹' ↑s

case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ ↑t2 ⊆ ↑s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ((mapDomain g l).sum fun i a ↦ a • id i) ∈ s

Tactic:
Finsupp.sum_mapDomain_index

Goal state after:
case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (l.sum fun a m ↦ m • id (g a)) ∈ s

case a.refine_2.left.h_zero
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M), 0 • id b = 0

case a.refine_2.left.h_add
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
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
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
w✝¹ : ↥p
w✝ : ↥q
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ (ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = χ (↑w✝¹ + ↑w✝)

Tactic:
simp [ofIsCompl, hφ, hψ]

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

Goal state before:
pp: case coe
s : Set ℕ∞
h : s.Infinite
x : ℕ
hx : ↑x < ⊤
⊢ ∃ a ∈ s, ↑x < a

Tactic:
| coe x =>

Goal state after: