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

Goal state before:
pp: a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ op a o = o

Tactic:
apply H.strictMono.le_apply.antisymm'
  rw [H.apply_of_isSuccLimit ho', Ordinal.iSup_le_iff]
  exact fun ⟨b, hbo⟩ ↦ (ho hao hbo).le

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

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ 0^[n✝ + 1] a ≤ 0^[0] a

Tactic:
· rw [Function.iterate_succ']
    simp

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

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun x ↦ a + x) b

Tactic:
rw [← nfp_add_zero]

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) 0 ≤ nfp (fun x ↦ a + x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) b ≤ a ^ ω

pp: case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x ↦ a * x) b

Tactic:
· apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]

Goal state after:
case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x ↦ a * x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Goal state after:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o

Tactic:
apply (lt_succ _).trans_le

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ succ (op a b) ≤ ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Goal state after:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

case inr
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o

Tactic:
apply (lt_succ _).trans_le

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ succ (op a b) ≤ ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 * b)

pp: case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
· rw [zero_mul]
    exact isPrincipal_zero

Goal state after:
case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Goal state after:
case inl
b : Cardinal.{u_1}
⊢ 0 * b ≤ max (max 0 b) ℵ₀

case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
| o.cof

Tactic:
← type_toType o,

Goal state after:
o : Ordinal.{u_1}
| (typeLT o.ToType).cof
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
⊢ r ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩

Tactic:
· apply (trichotomous_of r _ _).resolve_right
    rintro (_ | hxy')
    · simp_all [Subtype.coe_inj]
    · obtain ⟨x, z, hz, rfl⟩ := x
      exact (hz _ hxy').asymm hxy

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preBeth o = ⨆ a, preBeth ↑a

Tactic:
rw [preBeth]
  apply (ciSup_mono bddAbove_of_small fun _ ↦ (cantor _).le).antisymm'
  rw [ciSup_le_iff' bddAbove_of_small]
  intro a
  rw [← preBeth_add_one]
  exact le_ciSup bddAbove_of_small (⟨_, ho.succ_lt a.2⟩ : Iio o)

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

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ (b + 1)).card ≤ max a.card (b + 1).card

Tactic:
| add_one b IH =>

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : ω ≤ b
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
  · apply (card_le_card <| opow_le_opow_left b (natCast_lt_omega0 n).le).trans
    apply (card_opow_le_of_omega0_le_left le_rfl _).trans
    simp [hb]
  · exact card_opow_le_of_omega0_le_left ha b

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
by
  rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H
  rw [H]
  exact cof_blsub_le_lift.{u, v} f

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

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
s : Set α
hs : Bounded r s
⊢ False

Tactic:
exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof

Tactic:
rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]

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

Goal state before:
pp: α β : Type u
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β

Tactic:
rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]

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

Goal state before:
pp: α β : Type u
⊢ #(α ↪ β) = 0 ↔ #β < #α

Tactic:
rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ¬(ℵ_ (o + 1)).IsSingular

Tactic:
by
  simp [← succ_aleph]

Goal state after:
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 := 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
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
j : ι
⊢ (b.repr ((linearCombination R v) l.some)) j = (b.repr ((linearCombination R v) l'.some)) j

Tactic:
by
      obtain rfl | ne := eq_or_ne i j
      · simp_rw [repr_eq_zero]
      simpa [single_apply, ne] using congr(b.repr $z j)

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

Goal state before:
pp: α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑sᶜ = #↑tᶜ

Tactic:
← lift_inj.{u, u}

Goal state after:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∈ {i}
⊢ (single i (x i)) j = x j

pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j

Tactic:
· rw [(id h : j = i), single_eq_same]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j
Module: Mathlib.Data.DFinsupp.BigOperators

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

Tactic:
by
        simp +contextual [h_zero]

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

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

Tactic:
by
        simp +contextual [h_zero]

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

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

Tactic:
by
        simp +contextual [h_zero]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : i ∉ v.support
⊢ f i (v i) = 1

Tactic:
mem_support_iff,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : ¬v i ≠ 0
⊢ f i (v i) = 1
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
⊢ f i = 0

Tactic:
mem_support_iff,

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 : ¬f i ≠ 0
⊢ 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 : ι) → 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 ∉ g.support
hf : f i = 0
⊢ g i = 0

Tactic:
mem_support_iff,

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 : ¬g i ≠ 0
hf : f i = 0
⊢ g i = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ i ∉ sf

Tactic:
simpa using hi

Goal state after:
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 →+ γ
| sumZeroHom fun i_1 ↦ ↑(Pi.single i φ i_1)

Tactic:
enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i✝ : ι
φ : β i✝ →+ γ
i : ι
| Pi.single i✝ (↑φ) i
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ (⨆ i, (U i).dualAnnihilator).dualCoannihilator

Tactic:
dualCoannihilator_iSup_eq

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ x ∉ μ.support

Tactic:
mem_support_iff,

Goal state after:
case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ ¬μ x ≠ 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : x ∉ μ.support
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
mem_support_iff,

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ¬μ x ≠ 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
mem_support_iff,

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : ¬(DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x ≠ 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
iSupIndep_iff_forall_dfinsupp

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : iSupIndep p
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
iSupIndep_iff_forall_dfinsupp

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
    DFunLike.congr_fun this φ
  ext
  simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
l : List (Set α)
a : α
⊢ a ∈ l.prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l

Tactic:
induction l using List.ofFnRec with | _ n f
   =>  _ 

Goal state after:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f
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 β
⊢ image2 f (↑s) (↑t ∪ ↑t') = image2 f ↑s ↑t ∪ image2 f ↑s ↑t'

Tactic:
exact image2_union_right

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

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

Tactic:
card_union_of_disjoint h

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

Goal state before:

Tactic:
(x * single m r).coeff m₁
    _ = x.coeff.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [coeff_mul]
    _ = x.coeff.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by gcongr; simp [*]
    _ = x.coeff m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]

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

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
coeff_mul

Goal state after:
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then r₁ * r₂ else 0) =
    x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i) = single (m i * ∏ x ∈ s, m x) (∏ i ∈ cons i s hi, r i)

Tactic:
prod_cons

Goal state after:
R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i) = single (m i * ∏ x ∈ s, m x) (r i * ∏ x ∈ s, r x)
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
⊢ g₁ = g₂

Tactic:
| _ s ih =>

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (insert a s).sort r = a :: s.sort r

Tactic:
rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r

Tactic:
X,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * (monomial 1) 1 = (monomial (n + 1)) r
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) a * X = (monomial (n + 1)) a

Tactic:
X,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) a * (monomial 1) 1 = (monomial (n + 1)) a
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
X,

Goal state after:
R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ ((monomial 1) 1).support = ∅