mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr.left
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
case inr.left
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ (embDomain f (x * y)).coeff (f g) = (embDomain f x * embDomain f y).coeff (f g)

Tactic:
simp only [coeff_mul, embDomain_coeff]

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2 =
    ∑ ij ∈ antidiagonal ⋯ ⋯ (f g), (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: case refine_1
x d : ℝ≥0
h : x ≤ x + d
⊢ ∃ s, x + d = x + star s * s

Tactic:
refine ⟨sqrt d, ?_⟩

Goal state after:
case refine_1
x d : ℝ≥0
h : x ≤ x + d
⊢ x + d = x + star (sqrt d) * sqrt d
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (a - b) + f b - f b = f (a - b)

Tactic:
add_tsub_cancel_right

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (a - b) = f (a - b)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊥
⊢ A = B ∨ B = ⊤

pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊤
⊢ A = B ∨ B = ⊤

Tactic:
all_goals
    replace h := congr(primeSpectrumEquiv A $h)
    simp_all

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ sInf {r | -x < f r} = sInf (-{r | f r < x})

Tactic:
congr 1

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ {r | -x < f r} = -{r | f r < x}
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨a', ⋯⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))

Tactic:
rw [← ha']

Goal state after:
case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨a', ⋯⟩ = (↑f).toFun ⟨a', ha'mem⟩
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
a✝ : Nontrivial R
hm : n ≤ n
⊢ 1 = q.coeff n

Tactic:
hq.2

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
a✝ : Nontrivial R
hm : n ≤ n
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

Tactic:
exact H.coeff_eq (isMonicOfDegree_add_add_two ..) (by lia)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

Tactic:
← mul_one n

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree (n * 1)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ ((aeval (X - C r)) p).IsMonicOfDegree n

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg]
  exact aeval_add hp (-r)

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
⊢ ∀ (a : M),
    ArchimedeanClass.mk a = (withTopOrderIso M) (ofLex ((f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) a)).orderTop

Tactic:
simp_rw [LinearPMap.mk_apply] at harch
    simp [harch]

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

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree + p.natDegree - p.natDegree ≤ n

Tactic:
add_tsub_cancel_right

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.coeff (p.natDegree + p.natTrailingDegree - p.natTrailingDegree) = p.coeff p.natDegree

Tactic:
add_tsub_cancel_right

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natDegree = p.coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ MvPolynomial.C (MvPolynomial.coeff m q) * (m.prod fun i k ↦ ![X, 1] i ^ k).homogenize n =
    MvPolynomial.C (MvPolynomial.coeff m q) * m.prod fun n e ↦ MvPolynomial.X n ^ e

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ (m.prod fun i k ↦ ![X, 1] i ^ k).homogenize n = m.prod fun n e ↦ MvPolynomial.X n ^ e
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ v + 0 = v

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ v = v
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ u + 0 = u

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ u = u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + 0 + 0)
hy : IsUnit (y + 0)
hz : IsUnit z
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
add_zero

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hz : IsUnit z
hx : IsUnit x
hy : IsUnit y
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p' + 0

Tactic:
add_zero

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: case h.one
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ (mk rels) 1 ∈ closure (range (of rels))

Tactic:
| one =>

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 }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u) =
    (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u)

Tactic:
congr 1

Goal state after:
case e_a
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 }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u
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 }
z w : QuadraticAlgebra R a b
⊢ z.re • 1 + w.re • 1 + z.im • ↑u + w.im • ↑u = z.re • 1 + z.im • ↑u + w.re • 1 + w.im • ↑u

Tactic:
congr 1

Goal state after:
case e_a
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 }
z w : QuadraticAlgebra R a b
⊢ z.re • 1 + w.re • 1 + z.im • ↑u = z.re • 1 + z.im • ↑u + w.re • 1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case e_a
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 }
z w : QuadraticAlgebra R a b
⊢ z.re • 1 + (w.re • 1 + z.im • ↑u) = z.re • 1 + (z.im • ↑u + w.re • 1)

Tactic:
congr 1

Goal state after:
case e_a.e_a
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 }
z w : QuadraticAlgebra R a b
⊢ w.re • 1 + z.im • ↑u = z.im • ↑u + w.re • 1
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:
by
  ext <;> grind [trace_def]

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₃
⊢ (Basis.self R).compHom q.liftHom = q

Tactic:
ext <;> simp [Basis.lift]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r a b
⊢ Rel r (a - c) (b - c)

Tactic:
simp only [sub_eq_add_neg, h.add_left]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
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
a b x✝ y✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ * c) (y✝ * d)

Tactic:
refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_

Goal state after:
case rel
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
a b x✝ y✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y✝ * c) (y✝ * d)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a✝ : α
⊢ (single a (f.coeff a) + (erase a) f).coeff a✝ = f.coeff a✝

Tactic:
simp [ coeff_add, Finsupp.single_add_erase]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ 0 • { toQuot := Quot.mk (Rel r) a✝ } = 0

Tactic:
simp [smul_quot, ← zero_quot]

Goal state after:
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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
F : RingQuot s →ₐ[S] B
⊢ (fun f' ↦ preLiftAlgHom S ⋯) ((fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) F) = F

Tactic:
by
      ext
      simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
                 AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk,
                 MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
have pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    have P_sa : star P = P := by
      simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]
    have Q_sa : star Q = Q := by
      simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]
    have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
    have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
    positivity

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
x : ↑↑Z.toPresheafedSpace
e : ({ hom := { base := g, c := gc } } ≫ f).hom = ({ hom := { base := g, c := hc } } ≫ f).hom
⊢ PresheafedSpace.Hom.stalkMap ({ base := g, c := gc } ≫ f.hom) x =
    PresheafedSpace.Hom.stalkMap ({ base := g, c := hc } ≫ f.hom) x

Tactic:
congr 1

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := gc }) ⋯.choose =
    PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := hc }) ⋯.choose

Tactic:
congr 1

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 Y.toPresheafedSpace

Tactic:
rw [← InducedCategory.comp_hom, f.inv_hom_id, SheafedSpace.id_hom]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
⊢ Continuous fun x ↦ x.elim

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
⊢ ∀ (g h : Z ⟶ X.restrict hf), g ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g = h

Tactic:
g₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ : Z ⟶ X.restrict hf
⊢ ∀ (h : Z ⟶ X.restrict hf), g₁ ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g₁ = h
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ sheafedSpaceMap (𝟙 R) = 𝟙 (sheafedSpaceObj R)

Tactic:
by
  ext : 1
  · exact Spec.topMap_id R
  · ext
    dsimp
    rw [comap_id (by simp)]
    simp
    rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ f.c.app (op (⋯.functor.obj (unop U))) ≫
      X.presheaf.map (((Opens.map f.base).map (⋯.functor.map i.unop)).op ≫ eqToHom ⋯) =
    f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map (𝟙 ↑X)).map i.unop).op)

Tactic:
congr 1

Goal state after: