mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      ((monomial P.natDegree) (P.coeff d) - (monomial P.natDegree) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) (η * P.leadingCoeff)) -
      (monomial P.natDegree) P.nextCoeff

Tactic:
rw [leadingCoeff, nextCoeff_of_natDegree_pos (hd ▸ d.succ_pos), hd, Nat.add_sub_cancel]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (d + 1 + 1)) (P.coeff (d + 1)) -
      ((monomial (d + 1)) (P.coeff d) - (monomial (d + 1)) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (d + 1 + 1)) (P.coeff (d + 1)) - (monomial (d + 1)) (η * P.coeff (d + 1))) -
      (monomial (d + 1)) (P.coeff d)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

Tactic:
smul_sum,

Goal state after:
case inr.refine_2.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = ∑ x ∈ Ico q (p.natDegree + 1), q ! • (aeval r) (c x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : x ∈ Ico 0 q ∧ x ∈ Ico q (p.natDegree + 1)
⊢ False

Tactic:
mem_Ico,

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ x ∈ Ico q (p.natDegree + 1)
⊢ False
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝ : QuadraticAlgebra R a b
⊢ 1 • x✝ = x✝

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ 0 • x = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
⊢ QuadraticAlgebra.C ↑0 = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ QuadraticAlgebra.C ↑(n + 1) = QuadraticAlgebra.C ↑n + 1

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
H : ∀ {P : R[X]}, P ≠ 0 → P.natDegree = d → 0 < P.leadingCoeff → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
h_lC : ¬0 < P.leadingCoeff
⊢ -P ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
H : ∀ {P : R[X]}, P ≠ 0 → P.natDegree = d → 0 < P.leadingCoeff → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
h_lC : ¬0 < P.leadingCoeff
⊢ (-P).natDegree = d

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
r : R
⊢ ((algebraMap R (QuadraticAlgebra R a b)) r).re • 1 + ((algebraMap R (QuadraticAlgebra R a b)) r).im • ↑u =
    (algebraMap R A) r

Tactic:
by
        simp [← Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 0 * x✝ = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 0 = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 1 * x✝ = x✝

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 1 = x✝

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ QuadraticAlgebra.C ((algebraMap S R) 1) = 1

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R) (x * y)) =
    QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ QuadraticAlgebra.C ((algebraMap S R) 0) = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R) (x + y)) =
    QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z = 1 ↔ (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 1

Tactic:
simp [← algebraMap_inj (R := R) (a := a) (b := b)]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) (trace z) = z + star z

Tactic:
ext <;> grind [trace_def]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹ = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y

Tactic:
← self_distrib

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x ◃ x ◃⁻¹ y = x ◃ x ◃ x ◃⁻¹ y
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } = c₃ • 1

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₁ • 1) + F (c₂ • q.i) = c₁ • 1 + c₂ • F q.i

Tactic:
map_smul,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ c₁ • F 1 + F (c₂ • q.i) = c₁ • 1 + c₂ • F q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ c₁ • F 1 + F (c₂ • q.i) = c₁ • 1 + c₂ • F q.i

Tactic:
map_smul,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ c₁ • F 1 + c₂ • F q.i = c₁ • 1 + c₂ • F q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₃ • 1) = c₃ • 1

Tactic:
map_smul,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ c₃ • F 1 = c₃ • 1
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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
⊢ ∀ a ∈ Ideal.ofRel r, (mkRingHom r) a = 0

Tactic:
refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h

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

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

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

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
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
⊢ Function.Involutive (star' r hr)

Tactic:
rintro ⟨⟨⟩⟩
    simp [star'_quot]

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ ∃ α, u = α • v

pp: case inr
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ∃ α, u = α • v

Tactic:
· exact ⟨⟨y, by simp [mem_iff, this, mul_comm y]⟩, by ext; exact huv⟩

Goal state after:
case inr
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ∃ α, u = α • v
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : { base := base, c := c }.base = { base := base', c := c' }.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }

Tactic:
dsimp at w

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : base = base'
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ ContinuousAt f x

Tactic:
dsimp at w

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : Continuous fun x ↦ f (i x)
⊢ ContinuousAt f x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.inv.c.app
            (op
              ((Opens.map
                    ((forget C).mapIso
                          (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj
                (unop (op U)))) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
congr_app (Iso.symm_inv _)

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
              (op
                ((Opens.map
                      ((forget C).mapIso
                            (colimit.isoColimitCocone
                                { cocone := colimitCocone F,
                                  isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj
                  (unop (op U)))) ≫
            (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑R
x : ↥(Spec R)
this : (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ f ''ᵁ ⨆ i, s i = ⨆ i, f ''ᵁ s i

Tactic:
ext : 1
  simp [Set.image_iUnion]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ Presieve.singleton f ∈ P.precoverage.coverings Y ∧ Presieve.singleton f f

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
⊢ IsPullback g iU iV f

Tactic:
by
  let e := IsOpenImmersion.isoOfRangeEq (pullback.snd iV f) iU
    (by simpa [range_pullbackSnd] using congr(($H').1))
  convert!
    (IsPullback.of_horiz_isIso
          (show CommSq e.inv iU (pullback.snd iV f) (𝟙 X) from ⟨by simp [e]⟩)).paste_horiz
      (IsPullback.of_hasPullback iV f)
  simp [← cancel_mono iV, e, pullback.condition, H]

Goal state after: