mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : 0 * 0 + s ≠ 0
⊢ IsSumNonzeroSq (0 * 0 + s)

pp: case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
·

Goal state after:
case sq_add.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : 0 * 0 + s ≠ 0
⊢ IsSumNonzeroSq (0 * 0 + s)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
·

Goal state after:
case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inr.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s a : R
ne_a : a ≠ 0
hs✝ : IsSumSq 0
ih : 0 ≠ 0 → IsSumNonzeroSq 0
hs : a * a + 0 ≠ 0
⊢ IsSumNonzeroSq (a * a + 0)

pp: case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
·

Goal state after:
case sq_add.inr.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s a : R
ne_a : a ≠ 0
hs✝ : IsSumSq 0
ih : 0 ≠ 0 → IsSumNonzeroSq 0
hs : a * a + 0 ≠ 0
⊢ IsSumNonzeroSq (a * a + 0)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
·

Goal state after:
case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.a
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ a✝ * a✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

pp: case sq_add.a
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
·

Goal state after:
case sq_add.a
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ a✝ * a✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ 1 < 2

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x + y = x + y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x + y = x + y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x + y = x + y

pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x + y = x + y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y

Tactic:
·

Goal state after:
case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
⊢ 0 * (b + c) = 0 * b + 0 * c

pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
a✝ : α
⊢ ↑a✝ * (b + c) = ↑a✝ * b + ↑a✝ * c

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
⊢ 0 * (b + c) = 0 * b + 0 * c
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c

Tactic:
cases a; · rfl
    cases b <;> cases c <;> try rfl
    exact congr_arg some (left_distrib _ _ _)

Goal state after:
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0

pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
a✝ : α
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS ↔ T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

pp: case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
·

Goal state after:
case refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1.inl
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a

pp: case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
·

Goal state after:
case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)
⊢ T ∈ (toEndRingHom α).rangeS
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_2.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = a * (↑T).toFun b

pp: case refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b

Tactic:
·

Goal state after:
case refine_2.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = a * (↑T).toFun b
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b

Tactic:
·

Goal state after:
case refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case mp
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α → R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

pp: case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Tactic:
·

Goal state after:
case mp
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α → R a = L a ∧ L a ∈ (toEndRingHom α).rangeS
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Tactic:
·

Goal state after:
case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k✝ : Type u_1
G : Type u_2
H✝ : Type u_3
inst✝¹⁸ : CommSemiring k✝
inst✝¹⁷ : Monoid G
inst✝¹⁶ : Monoid H✝
A✝ : Type u_4
B : Type u_5
inst✝¹⁵ : Semiring A✝
inst✝¹⁴ : Algebra k✝ A✝
inst✝¹³ : Semiring B
inst✝¹² : Algebra k✝ B
inst✝¹¹ : MulSemiringAction G k✝
inst✝¹⁰ : SMulCommClass G k✝ k✝
k : Type u_6
A : Type u_7
inst✝⁹ : CommSemiring k
inst✝⁸ : Semiring A
inst✝⁷ : Algebra k A
H : Type u_8
F : Type u_9
inst✝⁶ : Monoid H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
inst✝³ : MulSemiringAction G A
inst✝² : MulSemiringAction H A
inst✝¹ : SMulCommClass G k A
inst✝ : SMulCommClass H k A
f : F
hf : ∀ (a : G) (x : A), a • x = f a • x
⊢ ∀ (r : k),
    (↑↑(mapDomainRingHom hf)).toFun ((algebraMap k (SkewMonoidAlgebra A G)) r) =
      (algebraMap k (SkewMonoidAlgebra A H)) r

Tactic:
by simp [mapDomainRingHom]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
·

Goal state after:
case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
·

Goal state after:
case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ ((erase a) f).support

pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ f.coeff a ≠ 0

pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a) f)

Tactic:
·

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ ((erase a) f).support
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ f.coeff a ≠ 0

pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a) f)

Tactic:
·

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ f.coeff a ≠ 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a) f)

Tactic:
·

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a) f)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : NonAssocSemiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
⊢ f = g

Tactic:
by
  ext x
  rcases mkRingHom_surjective r x with ⟨x, rfl⟩
  exact (RingHom.congr_fun w x :)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, (mkRingHom r) x = 0

pp: case refine_2
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ (mkRingHom r) 0 = 0

pp: case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (x y : B),
    x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) x = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (x + y) = 0

pp: case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
·

Goal state after:
case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, (mkRingHom r) x = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_2
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ (mkRingHom r) 0 = 0

pp: case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (x y : B),
    x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) x = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (x + y) = 0

pp: case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
·

Goal state after:
case refine_2
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ (mkRingHom r) 0 = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (x y : B),
    x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) x = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (x + y) = 0

pp: case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
·

Goal state after:
case refine_3
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (x y : B),
    x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) x = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (x + y) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
·

Goal state after:
case refine_4
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ (a x : B), x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} → (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0