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

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)

Tactic:
mul_assoc,

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
simpa [add_comm] using add_lt_add_iff_of_right_lt_aleph0 (a := a) (b := b) hc

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

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).card ≤ c

Tactic:
refine card_iSup_Iio_le ?_ fun i ↦ ?_

Goal state after:
case le_cof_ord.refine_1
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (succ c).ord.cof.ord.card ≤ c

case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ (↑(f i) + 1).card ≤ c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ erase i f + single i b = f - single i (f i) + single i b

Tactic:
erase_eq_sub_single f i

Goal state after:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f - single i (f i) + single i b = f - single i (f i) + single i b
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 : ι) → (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 ∈ (↑⟨sx, hx⟩).toFinset | f i ≠ 0} = {i ∈ (↑⟨sy, hy⟩).toFinset | f i ≠ 0}

Tactic:
dsimp only [Subtype.coe_mk, toFun_eq_coe] at *

Goal state after:
ι : 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 ∈ sx.toFinset | f i ≠ 0} = {i ∈ sy.toFinset | f i ≠ 0}
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
⊢ ∑ i ∈ (↑⟨sx, hx⟩).toFinset, (φ i) (f i) = ∑ i ∈ (↑⟨sy, hy⟩).toFinset, (φ i) (f i)

Tactic:
dsimp only [Subtype.coe_mk, toFun_eq_coe] at *

Goal state after:
ι : 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
⊢ ∑ i ∈ sx.toFinset, (φ i) (f i) = ∑ i ∈ sy.toFinset, (φ i) (f i)
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
have := (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
  rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this
  exact this

Goal state after:
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)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ((lsum ℕ) fun i ↦ (p i).subtype) (single i x)
⊢ x = 0

Tactic:
have := DFunLike.ext_iff.mp (h hv) i

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)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ((lsum ℕ) fun i ↦ (p i).subtype) (single i x)
this : (erase i v) i = (single i x) i
⊢ x = 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
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s = 0 ∧ t = 0

Tactic:
specialize h' (a • s + c • t) (b • s + d • t) (by simp only [← hst, smul_add, add_smul,
    smul_assoc, smul_comm a s, smul_comm c t, smul_comm b s, smul_comm d t]; abel)

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
s t : R
h' : a • s + c • t = 0 ∧ b • s + d • t = 0
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: 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
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
this : (a * d) • s = (b * c) • s
hs : ¬s = 0
⊢ False

Tactic:
exact h (_root_.smul_left_injective S hs ‹_›)

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ S.mkQ x ∈ (S.mapQ T LinearMap.id h).ker

Tactic:
rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (LinearMap.id x) = 0
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
⊢ a • f = (RingHom.pi fun i ↦ algebraMap R (A i)) a * f

Tactic:
ext; simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
t : R
v : ι → R
⊢ ⇑(algebraMap R A) ∘ (t • v) = (RingHom.id R) t • ⇑(algebraMap R A) ∘ v

Tactic:
ext; simp [Algebra.smul_def]

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

Goal state before:
pp: X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support

Tactic:
apply support_zsmul k _ a

Goal state after:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0
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
x : V
⊢ LinearIndependent K (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LinearIndependent K (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ∧
        Disjoint (span K (range (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)))
          (K ∙ (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
@linearIndependent_unique_iff PUnit,

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
⊢ LinearIndependent K (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ≠ 0 ∧
        Disjoint (span K (range (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)))
          (K ∙ (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
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
x : V
⊢ (LinearIndependent K fun o ↦ o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u'} ι).symm, linearIndependent_sum,
    @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]
  dsimp [(· ∘ ·)]
  refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩
  rintro rfl
  exact h.2 (zero_mem _)

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)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

Tactic:
by
  conv_rhs => rw [← sum_coeff_single a, ← sum_coeff_single b]
  simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
  refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
  simp [mul_assoc, (h_comm hy).left_comm]

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✝³ : 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))
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

Tactic:
by
  conv_rhs => rw [← sum_coeff_single a, ← sum_coeff_single b]
  simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
  refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
  simp [mul_assoc, (h_comm hy).left_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit ↑s ↔ IsUnit s

Tactic:
isUnit_iff,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit ↑s ↔ ∃ a, s = {a} ∧ IsUnit a
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' * b⁻¹ = b0 * b⁻¹
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
mul_right_cancel_iff

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * (X * p) = p * X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ p * X ^ n * X = p * X ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ p * (X ^ n * X) = p * X ^ (n + 1)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
mul_assoc,

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * (a' * (b' * b⁻¹)) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * (X ^ n * q) = p * q * X ^ n
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * ((a0, b0).1 * (a0, b0).2 * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
mul_assoc,

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * ((a0, b0).1 * ((a0, b0).2 * b⁻¹)) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

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

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
⊢ C a * X = C a * X ^ 1
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:
rw [C_mul_X_pow_eq_monomial, support_monomial n h]

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

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * c3 * (d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
mul_assoc,

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c3 * (d3 * c2⁻¹)) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
by
  simp [sum]

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

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c1 * d2 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
mul_assoc,

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c1 * (d2 * c2⁻¹)) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x✝ : ↥p
x : E
hx : ↑f x ∈ p
⊢ ↑((codRestrict p ↑f ⋯) ↑⟨↑f x, hx⟩) = ↑⟨↑f x, hx⟩

Tactic:
exact DFunLike.congr_fun f.2.1 x

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

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + a

Tactic:
by
  simp [add_comm, add_iSup]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
      (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).castSucc =
    p.last

pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head

Tactic:
· convert! Fin.append_left p q _

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n ∈ ⊥
⊢ (f m) n ∈ ⊥

Tactic:
by
      rw [Submodule.mem_bot] at hn
      rw [hn, map_zero]; simp only [mem_bot]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ((RelSeries.eraseLast p).last, x) ∈ {(a, b) | a < b}

Tactic:
apply lt_of_lt_of_le
      · apply p.step ⟨p.length - 1, by lia⟩
      · convert! hlast
        simp only [Fin.succ_mk, RelSeries.last, Fin.last]
        congr; lia

Goal state after: