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

Goal state before:
pp: m n : ℕ
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
obtain hm | hm := le_or_gt m 1
  case inl => rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]
  obtain rfl | hn := eq_or_ne n 0
  case inl => simp
  rw_mod_cast [eq_comm, log_eq_iff (mod_cast hm) (mod_cast hn), ← Nat.log_eq_iff (.inr ⟨hm, hn⟩)]

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
rw [isPrincipal_add_iff_add_self_lt]

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
by
  obtain rfl | rfl | rfl := le_two_iff.1 ho
  exacts [isPrincipal_zero, isPrincipal_mul_one, isPrincipal_mul_two]

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
· exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

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

Goal state before:
pp: case a
a : Ordinal.{u_1}
ha : a ∈ Iio ω
⊢ preBeth ↑⟨a, ha⟩ ≤ ℵ₀

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 ha

Goal state after:
case a
n : ℕ
ha : ↑n ∈ Iio ω
⊢ preBeth ↑⟨↑n, ha⟩ ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u, v} #↑(sSup (range ((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm))) ≤ lift.{u, v} c

Tactic:
apply ((mk_iUnion_le_lift _).trans _).trans_eq (mul_eq_self (aleph0_le_lift.2 hc))

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} #o.ToType * ⨆ i, lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c * lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by
  by_cases! hc : c < ℵ₀
  · obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
    rw [card_le_nat]
    refine ciSup_le' fun i ↦ ?_
    simpa using hf i
  · rw [← Cardinal.lift_le.{u}]
    apply (lift_card_iSup_le_sum_card ..).trans ((sum_le_lift_mk_mul_iSup_lift _).trans _)
    rw [← mul_eq_self hc, Cardinal.lift_mul]
    apply mul_le_mul' hι (ciSup_le' _)
    simpa [← lift_card]

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < o
⊢ a < lsub f

Tactic:
rw [← type_toType o] at ha

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < typeLT o.ToType
⊢ a < lsub f
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b

Tactic:
constructor <;> contrapose! <;> simp [add_le_add_iff_of_lt_aleph0 hc]

Goal state after:
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
⊢ Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof

Tactic:
rw [Cardinal.lift_max]

Goal state after:
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
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ ℵ₀ ≤ κ

Tactic:
simpa using h₁

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

Goal state before:
pp: κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ κ ≤ κ.ord.cof

Tactic:
by simpa [← lift_le.{u, v}]

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

Goal state before:
pp: case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑s ≤ #↑(f ⁻¹' {a})

Tactic:
rw [← ha, @preimage_comp _ _ _ Subtype.val f]

Goal state after:
case h
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
a : α
ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s
⊢ #↑(Subtype.val ⁻¹' f ⁻¹' {a}) ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ Nonempty ((α → Bool) ↪ Perm (α × Bool))

Tactic:
refine ⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (fun x ↦ (x.1, f x.1 ^^ x.2)) ((fun x ↦ (x.1, f x.1 ^^ x.2)) x) = x

case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
⊢ f = g
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < #α ^ #↑s

Tactic:
← prod_const'

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < prod fun x ↦ #α
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (r • f)) i✝ = r • (comapDomain' h hh' f) i✝

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (r • f) (h i✝) = r • (comapDomain' h hh' f) i✝
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
x✝ : a ∈ ↑(fs ⟨i, ⋯⟩) ∨ (f ↑⟨i, ⋯⟩).toFun a = 0
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with

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

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ 0 (h i✝) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f) i✝ + (comapDomain' h hh' g) i✝

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (f + g) (h i✝) = (comapDomain' h hh' f) i✝ + (comapDomain' h hh' g) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (f + g) (h i✝) = (comapDomain' h hh' f) i✝ + (comapDomain' h hh' g) i✝

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (f + g) (h i✝) = f (h i✝) + (comapDomain' h hh' g) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (f + g) (h i✝) = f (h i✝) + (comapDomain' h hh' g) i✝

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (f + g) (h i✝) = f (h i✝) + g (h i✝)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h ⋯ (comapDomain' ⇑h.symm ⋯ f)) i) = f i

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h.symm ⋯ f) (h i)) = f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h.symm ⋯ f) (h i)) = f i

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) (f (h.symm (h i))) = f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (comapDomain' ⇑h.symm ⋯ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f)) k = f k

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f) (h.symm k) = f k
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h ⋯ f) (h.symm k)) = f k

Tactic:
comapDomain'_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (Equiv.cast ⋯) (f (h (h.symm k))) = f k
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Tactic:
by
  ext
  simp only [mapRange_apply f, coe_add, Pi.add_apply, hf']

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

Goal state before:
pp: case refine_1
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : m ∈ (dualMap f).range
r : Dual R R
hr : (dualMap f) r = m
⊢ r 1 • f = m

pp: case refine_2
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m

Tactic:
· ext; simp [dualMap_apply', ← hr]

Goal state after:
case refine_2
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m

Tactic:
· ext; simp [dualMap_apply', ← hr]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s • u • x + t • u • y = 0

Tactic:
hst

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
⊢ s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0

Tactic:
hst

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ (d • 1) • (a • x + b • y) + (-b • 1) • (c • x + d • y) = 0

Tactic:
simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]

Goal state after:
case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ (b * c) • x + (b * d) • y + ((-b * c) • x + (-b * d) • y) = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' s)

Tactic:
by
  classical
    rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff'.mpr fun s g hrel i hi ↦ ?_

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
s : Finset ι
g : ι → R
hrel : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 1 = ψ

Tactic:
ext; rw [mulShift_apply, one_mul]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (a * a_1)) =
    a.coeff.sum fun a c ↦ ↑f c * g a * b.coeff.sum fun a b ↦ ↑f b * g a

Tactic:
Finsupp.mul_sum

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (a * a_1)) =
    a.coeff.sum fun a c ↦ b.coeff.sum fun a_1 c_1 ↦ ↑f c * g a * (↑f c_1 * g a_1)
Module: Mathlib.Algebra.MonoidAlgebra.Lift

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (Multiplicative.ofAdd (a + a_1))) =
    a.coeff.sum fun a c ↦ ↑f c * g (Multiplicative.ofAdd a) * b.coeff.sum fun a b ↦ ↑f b * g (Multiplicative.ofAdd a)

Tactic:
Finsupp.mul_sum

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (Multiplicative.ofAdd (a + a_1))) =
    a.coeff.sum fun a c ↦
      b.coeff.sum fun a_1 c_1 ↦ ↑f c * g (Multiplicative.ofAdd a) * (↑f c_1 * g (Multiplicative.ofAdd a_1))
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

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

Tactic:
induction n generalizing a with
  | zero => simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
  | succ n ih =>
    simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
      mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]

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 : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
this : b₁ ∈ s ∩ ↑(insert b₁ t)
⊢ False

Tactic:
hst

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
this : b₁ ∈ ∅
⊢ False
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huH : UniqueMul (image (⇑f) A) (image (⇑f) B) aH bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG

Tactic:
by
  specialize huH (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)
  rw [← map_mul, he, map_mul, hae, hbe] at huH
  refine huG ?_ ?_ he <;> rw [mem_filter]
  exacts [⟨ha, (huH rfl).1⟩, ⟨hb, (huH rfl).2⟩]

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

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

Tactic:
support_zero

Goal state after:
R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ ∅ = ∅
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

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

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

Tactic:
← Polynomial.smul_C,

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

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

Tactic:
← Polynomial.smul_C,

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