mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) ≤ max (1 * A.valuation (↑b - 1)) (A.valuation (↑a - 1))

Tactic:
← A.valuation.map_one_add_of_lt ha,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) ≤ max (A.valuation (1 + (↑a - 1)) * A.valuation (↑b - 1)) (A.valuation (↑a - 1))
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a : WithTop α
⊢ 0 ≤ a.untop₀ ↔ 0 ≤ a

Tactic:
cases a with
  | top => tauto
  | coe a => simp

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

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
z : FiniteResidueField K
hz : 0 ≤ z
x y : FiniteElement K
h : mk x ≤ mk y
⊢ z * mk x ≤ z * mk y

Tactic:
induction z with

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
hz : 0 ≤ mk z
⊢ mk z * mk x ≤ mk z * mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
z : FiniteResidueField K
x y : FiniteElement K
h : mk x ≤ mk y
⊢ mk x + z ≤ mk y + z

Tactic:
induction z with

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G s ≤ stabilizer G (s ∪ t)

Tactic:
calc
      stabilizer G s
        ≤ stabilizer G s ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union

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
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ f (-r) < -x

Tactic:
apply lt_of_lt_stdPart

Goal state after:
case hx
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ 0 ≤ mk (-x)

case h
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ -r < stdPart (-x)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: 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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
⊢ StrictMono ↑(sSupFun hc)

Tactic:
intro x y h
  apply lt_of_sub_pos
  rw [← LinearPMap.map_sub]
  obtain hyx := (y - x).prop
  simp_rw [sSupFun, LinearPMap.domain_sSup] at hyx
  obtain ⟨f, hmem, hf⟩ :=
    (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hyx
  have : (sSupFun hc) (y - x) = f ⟨(y - x).val, hf⟩ :=
    LinearPMap.sSup_apply _ hmem ⟨(y - x).val, hf⟩
  rw [this]
  obtain ⟨f', _, hf'⟩ := (Set.mem_image _ _ _).mp hmem
  have hmono : StrictMono f := hf'.symm ▸ f'.prop.strictMono
  rw [show 0 = f 0 by simp]
  apply hmono
  rw [← Subtype.coe_lt_coe]
  simp [h]

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i Df + i Dg = i b ^ N * eval (i a * bf) (Polynomial.map i (f + g))

Tactic:
Polynomial.map_add,

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i Df + i Dg = i b ^ N * eval (i a * bf) (Polynomial.map i f + Polynomial.map i g)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i (Df + Dg) = i b ^ N * eval (i a * bf) (Polynomial.map i (f + g))

Tactic:
rw [map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp } =
    { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
      { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }

Tactic:
ext i
    by_cases h : i < n
    · simp [h]
    · simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp } =
    (RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }

Tactic:
ext i
    by_cases h : i < n
    · simp [h]
    · simp [h]

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

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

Tactic:
simp [Finsupp.prod_fintype, Finsupp.weight_apply, Finsupp.sum_fintype, Fin.prod_univ_two,
    Fin.sum_univ_two]

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous p.natDegree

Tactic:
simp [toTupleMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 0) = p * (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 1)

Tactic:
simp [toTupleMvPolynomial]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ ⊥ < (∏ i ∈ s, g i).degree

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ (∏ i ∈ s, g i).degree ≠ ⊥
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ)
      ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
    (h1 | h1)

Goal state after:
case inl
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = ↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
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✝ : AddMonoid R
⊢ AddMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_ <;> intros

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ (g i ^ n i).degree ≠ ⊥
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
⊢ ∀ (m : R) (x : QuadraticAlgebra R a b), 2 * (m • x).re + b * (m • x).im = (RingHom.id R) m • (2 * x.re + b * x.im)

Tactic:
by grind [smul_eq_mul]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
x : ι
hx : x ∈ s
⊢ (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1

Tactic:
rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ⇑f
a b : α
⊢ f (a * b) = a * f b

Tactic:
map_mul_left

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝⁸ : Monoid G
inst✝⁷ : Monoid H
inst✝⁶ : Semiring A
inst✝⁵ : CommSemiring k
inst✝⁴ : Algebra k A
inst✝³ : MulSemiringAction G A
inst✝² : MulSemiringAction H A
inst✝¹ : SMulCommClass G k A
inst✝ : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = e a • x
a : H
x : A
⊢ a • x = e.symm a • x

Tactic:
rw [he, MulEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = image (fun x_1 ↦ x * x_1) f.support

Tactic:
by
  refine subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
    simpa only [Finset.mem_image, exists_prop] using hy
  simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, Ne,
    zero_mul, ite_self, sum_zero, lx.eq_iff]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case of
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
r✝ : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r✝ x y → f x = f y
x : RingQuot r✝
a✝ b✝ x✝ y✝ : R
r : r✝ x✝ y✝
⊢ f x✝ = f y✝

Tactic:
exact h r

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
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) y = 0

Tactic:
rw [← su, map_sub, mkRingHom_rel h, sub_self]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case of
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 : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
x : RingQuot s
a✝ b✝ x✝ y✝ : A
r : s x✝ y✝
⊢ f x✝ = f y✝

Tactic:
exact h r

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Tactic:
by
  simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]
  rfl

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 := ⋯
Q : R := ⋯
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ √2 ^ 3 • 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)

Tactic:
simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos

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

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
⊢ StarAddMonoid R

Tactic:
apply e.injective.starAddMonoid <;> (intros; exact e.apply_symm_apply _)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g h : SkewMonoidAlgebra k G
⊢ f * g * h = f * (g * h)

Tactic:
induction f with
    | single x a => induction g with
      | single y b => induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
      | add => simp_all [add_mul, mul_add]
    | add => simp_all [add_mul]

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

Goal state before:
pp: 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
hvy : 1 • ↑v = (star y * y) • ↑v
⊢ ∃ α, u = α • v

Tactic:
rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero, eq_comm] at hvy

Goal state after:
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
hvy : star y * y = 1 ∨ ↑v = 0
⊢ ∃ α, u = α • v
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
⊢ IsUnit f

Tactic:
have ic : IsCompatible (sheaf X).obj V g := by
    intro x y
    apply section_ext X.sheaf (V x ⊓ V y)
    rintro z ⟨hzVx, hzVy⟩
    rw [germ_res_apply, germ_res_apply]
    apply (h z ((iVU x).le hzVx)).mul_right_inj.mp
    rw [← germ_res_apply X.presheaf (iVU x) z hzVx f]
    -- Porting note: change was not necessary in Lean3
    change X.presheaf.germ _ z hzVx _ * (X.presheaf.germ _ z hzVx _) =
      X.presheaf.germ _ z hzVx _ * X.presheaf.germ _ z hzVy (g y)
    rw [← map_mul, hg x, germ_res_apply X.presheaf _ _ _ f,
      ← germ_res_apply X.presheaf (iVU y) z hzVy f, ← map_mul, (hg y), map_one, map_one]

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
ic : IsCompatible (sheaf X).obj V g
⊢ IsUnit f
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x ⋯)) f)

Tactic:
exact hx

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ X.basicOpen f = U

Tactic:
apply le_antisymm
  · exact X.basicOpen_le f
  intro x hx
  rw [X.mem_basicOpen f x hx]
  exact RingHom.isUnit_map _ hf

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

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
s : (x : ↥(iSup U)) → T ↑x := fun x ↦ sf (index x) ⟨↑x, ⋯⟩
i : ι
x : ↥(Opposite.unop (Opposite.op (U i)))
⊢ (ConcreteCategory.hom ((X.presheafToTypes T).map (leSupr U i).op)) s x = sf i x

Tactic:
exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
a b : ↥X
⊢ a ≤ b ↔ b ⤳ a

Tactic:
by rfl

Goal state after: