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

Goal state before:
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:
rcases eq_zero_or_pos b with (rfl | hb₁')
    · rw [mul_zero]
      exact isPrincipal_zero
    · rw [← one_le_iff_pos] at hb₁'
      intro c d hc hd
      rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
      rcases hc with ⟨x, hx, hx'⟩
      rcases hd with ⟨y, hy, hy'⟩
      use x + y, hb hx hy
      rw [mul_add]
      exact Left.add_lt_add hx' hy'

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

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 2

Tactic:
intro a

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < 2 → b < 2 → (fun x1 x2 ↦ x1 * x2) a b < 2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk.hbc.inr
α : 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)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
rwa [IH _ this hq]

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

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

Tactic:
simp [← not_lt]

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

Goal state before:
pp: ⊢ StrictMono preBeth

Tactic:
intro a

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < b → preBeth a < preBeth b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ∀ (i : ↑(Iio o)), 2 ^ preBeth ↑i ≤ ⨆ x, preBeth ↑x

Tactic:
intro a

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : ↑(Iio o)
⊢ 2 ^ preBeth ↑a ≤ ⨆ x, preBeth ↑x
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rw [add_eq_max ha]
    exact le_max_left _ _

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

Goal state before:
pp: case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i ∈ Iio (⨆ i, f i + 1)

Tactic:
rw [mem_Iio]

Goal state after:
case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i < ⨆ i, f i + 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case zero
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ cof 0 ≤ (f 0).cof

Tactic:
| zero =>

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
hfc : ¬BddAbove (range fun x ↦ f x * c)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
simp [iSup, csSup_of_not_bddAbove, hf, hfc]

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ 0).card ≤ max a.card (card 0)

Tactic:
| zero =>

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

Goal state before:
pp: case inl.inl
n m : ℕ
⊢ (↑(n ^ m)).card ≤ max ℵ₀ (max (↑n).card (↑m).card)

Tactic:
card_nat

Goal state after:
case inl.inl
n m : ℕ
⊢ ↑(n ^ m) ≤ max ℵ₀ (max (↑n).card (↑m).card)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

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

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
⊢ StrictMono fun a ↦ ↑(n + 1 + 1) * a

Tactic:
intro a

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a : Cardinal.{u_1}
⊢ ∀ ⦃b : Cardinal.{u_1}⦄, a < b → (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
apply max_lt <;> simpa

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ o)

Tactic:
intro a

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < ω_ o → b < ω_ o → (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

Tactic:
intro a

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 + x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

Tactic:
intro a

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 * x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩

Tactic:
intro a

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a : α
⊢ ∀ ⦃a₂ : α⦄, (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) a₂ → a = a₂
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
intro a

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

Goal state before:
pp: case zero
ι : 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
⊢ 0 < c.ord → derivFamily f 0 < c.ord

Tactic:
| zero =>

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (c • x)) i = (c • mk s x) i

Tactic:
simp only [smul_apply, mk_apply]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
rw [h, single_zero, zero_add]
    exact H2

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

Goal state before:
pp: case inl.inl
ι : 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) ⟨i, j'⟩ = (single j' x) j'

Tactic:
rw [single_eq_same, single_eq_same]

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

Goal state before:
pp: case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
⊢ (single j' x) j' = (single ⟨i, j'⟩ x) ⟨i, j'⟩

Tactic:
rw [single_eq_same, single_eq_same]

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

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

Tactic:
by_cases h : i = i'

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

case neg
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : ¬i = i'
⊢ (mapRange f hf (single i b)) i' = (single i (f i b)) i'
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
by
    by_cases h : i = i'
    · subst i'
      simp
    · simp [h, hf]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)

Tactic:
refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))

Goal state after:
case refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

case refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset ∩ sy.toFinset, (φ x) (f x) = (φ x) (f x)

case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
rw [single_eq_same, single_eq_same]

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

Goal state before:
pp: case some.inl
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
⊢ (single j x) j = (single (some j) x) (some j)

Tactic:
rw [single_eq_same, single_eq_same]

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₂
hf : Function.Surjective ⇑f
⊢ Function.Injective ⇑f.dualMap

Tactic:
intro φ

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₂
hf : Function.Surjective ⇑f
φ : Dual R M₂
⊢ ∀ ⦃a₂ : Dual R M₂⦄, f.dualMap φ = f.dualMap a₂ → φ = a₂
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
⊢ GaloisConnection (⇑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ⇑OrderDual.ofDual)

Tactic:
intro a

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
⊢ ∀ (b : (Submodule R (Dual R M))ᵒᵈ),
    (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) b
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
⊢ ∀ (i : ι) (b : M i) (f : Π₀ (i : ι), M i),
    f i = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single i b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single i b + f)

Tactic:
intro a

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),
    f a = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
c d : R
h :
  ↑{i, j} ⊆ {i, j} →
    (∀ i_1 ∉ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0) →
      ∑ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 • f i_1 = 0 →
        ∀ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

Tactic:
simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ s • x = (r • l).eval

Tactic:
← hs,

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • x = (r • l).eval
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
⊢ (RingHom.pi fun i ↦ algebraMap R (A i)) a * f = f * (RingHom.pi fun i ↦ algebraMap R (A i)) a

Tactic:
by ext; simp [Algebra.commutes]

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

Goal state before:
pp: case hf
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ Injective fun ji ↦ f ji.fst ji.snd

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy

Goal state after:
case hf
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ (if ψ = 0 then ↑(card A) else 0) = 0 ↔ ψ ≠ 0

Tactic:
Ne.ite_eq_right_iff

Goal state after:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ¬ψ = 0 ↔ ψ ≠ 0

A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
| zero =>

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
f : Fin 2 → V
⊢ Fin.tail f default ≠ 0 ∧ f 0 ∉ span K (range (Fin.tail f)) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

Tactic:
range_unique,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default ≠ 0 ∧ f 0 ∉ K ∙ Fin.tail f default ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
ab : A × A
hab : ab.1 ∈ f.coeff.support ∧ ab.2 ∈ g.coeff.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.1 = (a0, b0).1

pp: case refine_1.refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
ab : A × A
hab : ab.1 ∈ f.coeff.support ∧ ab.2 ∈ g.coeff.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.2 = (a0, b0).2

Tactic:
exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
⊢ UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0

Tactic:
intro a

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A.preimage ⇑f ⋯ → b ∈ B.preimage ⇑f ⋯ → a * b = a0 * b0 → a = a0 ∧ b = b0
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
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ a :: s.val.sort r = a :: s.sort r

Tactic:
sort_val

Goal state after:
α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ a :: s.sort r = a :: s.sort r
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑(npowRec 0 s) = ↑s ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
⊢ Free R' M'

Tactic:
by
  let e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
  let I := Module.Free.ChooseBasisIndex R M
  obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M
  let e : M' ≃+ (I →₀ R') :=
    (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv)
  have he (x) : e x = Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
  let e' : M' ≃ₗ[R'] (I →₀ R') :=
    { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [e₁, he, map_smulₛₗ] }
  exact of_basis (.ofRepr e')

Goal state after: