mathlib-initiative/mathlib-tactics huggingface dataset:
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
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩))) ∈ f.toFun.range
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x))) ∈ (sSupFun hc).toFun.range

Tactic:
LinearMap.mem_range,

Goal state after:
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
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : ∃ y, f.toFun y = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
⊢ ∃ y, (sSupFun hc).toFun y = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
q₁ q₂ : R[X]
r₁ r₂ : Fin 0 → R[X]
hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree
hf : q₁ * g ^ 0 + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ 0 + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂

Tactic:
by simpa using hf

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

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, Fin.snoc rs₂ r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
| snoc rs₂ r₂
     => 

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, Fin.snoc rs₂ r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b cs).length ≤ (destutter' R a cs).length

Tactic:
exact (length_destutter'_congr cs hab).ge

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₁ r₂ : Fin (n + 1) → R[X]
hr₁ : ∀ (i : Fin (n + 1)), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ r₁ = r₂

Tactic:
cases r₁ using Fin.snocCases with | snoc rs₁ r₁
    cases r₂ using Fin.snocCases with | snoc rs₂ r₂
    simp only [Fin.sum_univ_castSucc, Fin.snoc_castSucc,
      Fin.val_castSucc, Fin.snoc_last, Fin.val_last] at hf
    rw [← add_rotate' (r₁ * g ^ n), ← add_rotate' (r₂ * g ^ n), pow_succ', ← mul_assoc, ← mul_assoc,
      ← add_assoc, ← add_assoc, ← add_mul, ← add_mul, ← mul_comm g, ← mul_comm g] at hf
    obtain ⟨hqr, hrs⟩ := ih
      (fun i => by simpa using hr₁ i.castSucc)
      (fun i => by simpa using hr₂ i.castSucc) hf
    obtain ⟨hq₁, hrr₁⟩ := div_modByMonic_unique q₁ r₁ hg ⟨rfl, by simpa using hr₁ (Fin.last n)⟩
    obtain ⟨hq₂, hrr₂⟩ := div_modByMonic_unique q₂ r₂ hg ⟨rfl, by simpa using hr₂ (Fin.last n)⟩
    exact ⟨hq₁.symm.trans (hqr ▸ hq₂), congrArg₂ Fin.snoc hrs (hrr₁.symm.trans (hqr ▸ hrr₂))⟩

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

Goal state before:
pp: case ha
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
rw [signVariations, signVariations, coeffList_eraseLead hpz]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign)
              (P.leadingCoeff ::
                (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList))))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
            (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.eraseLead.coeffList))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑(q ! * (q + 1).ascFactorial k) * (aeval r) p'

Tactic:
Nat.factorial_mul_ascFactorial

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

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
· rw [← mirror_inj, trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero] at hq
    rw [mul_comm q, ← q.mirror_mirror, q.mirror.mirror_mirror] at h
    rw [← mirror_inj, or_comm, ← mirror_eq_iff]
    exact
      irreducible_aux2 hkm hmn (lt_add_of_pos_left k (tsub_pos_of_lt hmn'))
        (lt_tsub_iff_right.mp ((tsub_lt_tsub_iff_left_of_le hmn'.le).mpr hkm')) u v w hp hq h

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

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

pp: case inr.inr
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror
hq : (-p).mirror = trinomial k m' n (↑x) (-↑v) ↑z
⊢ (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror

Tactic:
· exact Or.inr (Or.inl rfl)

Goal state after:
case inr.inr
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror
hq : (-p).mirror = trinomial k m' n (↑x) (-↑v) ↑z
⊢ (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror
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 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
⊢ s_nC_mul = -1

Tactic:
have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
      simp [*, ← hs_nC_mul, nextCoeff, coeff_X_sub_C_mul]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∈ (QuadraticAlgebra R a b)⁰ ↔ r ∈ R⁰

Tactic:
simp only [mem_nonZeroDivisors_iff_right]
  constructor
  · intro H x hxr
    rw [← algebraMap_inj, map_zero]
    apply H
    rw [← map_mul, hxr, map_zero]
  · intro h z hz
    rw [QuadraticAlgebra.ext_iff, re_zero, im_zero] at hz
    simp only [re_mul, algebraMap_re, algebraMap_im, mul_zero, add_zero, im_mul, zero_add] at hz
    simp [QuadraticAlgebra.ext_iff, re_zero, im_zero, h _ hz.left, h _ hz.right]

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n

Tactic:
cases n with
    | ofNat n => rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr
    | negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
by rw [← neg_mul]; exact AddSubmonoid.mul_mem_mul (M.neg_mem hm) hn

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).leadingCoeff = 1 ↔ P.leadingCoeff = 1

Tactic:
← int_leadingCoeff_eq,

Goal state after:
K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).leadingCoeff = 1 ↔ ↑(int ?R P ?hP).leadingCoeff = 1

case R
K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ Subring K

case hP
K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ ∀ (n : ℕ), P.coeff n ∈ ?R
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 α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact map_mul_left g (↑z) a

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

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

Tactic:
classical
  rw [f.coeff_update_apply, if_pos rfl]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
f g : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ f * g = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)

Tactic:
by
  ext
  simp [φ_iterate_apply, sum_def', coeff_mul, monomial, lsingle_apply, SkewMonoidAlgebra.coeff_sum']
  simp [SkewMonoidAlgebra.sum, Finsupp.single_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p = q

Tactic:
← mul_one p,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 1 = q
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
    star_eq_iff_star_eq, eq_comm]

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
u : (End R E)ˣ
hu : ↑u = f.ofConv
this : IsUnit (star (toConv ↑u)).ofConv
⊢ IsUnit (star f).ofConv

Tactic:
simpa [hu] using this

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

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ (P.and Q.toPrelocalPredicate).pred f

Tactic:
refine ⟨P.locality f ?_, Q.locality f ?_⟩ <;>
      (intro x; have ⟨V, hV, i, h⟩ := w x; use V, hV, i)
    exacts [h.1, h.2]

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

Goal state before:
pp: case w
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥↑U) → T ↑y
h : P.pred f
⊢ (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)

pp: case h
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥↑U) → T ↑y
h : P.pred f
⊢ (ConcreteCategory.hom (stalkToFiber P x)) ?w = f ⟨x, ⋯⟩

Tactic:
· exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩

Goal state after:
case h
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥↑U) → T ↑y
h : P.pred f
⊢ (ConcreteCategory.hom (stalkToFiber P x))
      ((ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑U) x ⋯)) ⟨f, h⟩) =
    f ⟨x, ⋯⟩
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
rw [invApp, ← Category.assoc, IsIso.comp_inv_eq, f.c.naturality]
  congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f.op) = inv (Scheme.Spec.map f.op)

Tactic:
← Scheme.Spec.map_inv

Goal state after:
R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f.op) = Scheme.Spec.map (inv f.op)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| ⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) ∘
      ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹'
    ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)

Tactic:
Function.comp_def,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| (fun x ↦
      (TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right))
        ((TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) x)) ⁻¹'
    ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
⊢ f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'

Tactic:
refine ⟨fun h ↦ ?_, f.image_mono⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ U ≤ U'
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
hf : ∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
x : (fun X ↦ X) Y
⊢ ∃ a, (ConcreteCategory.hom f) a = x

Tactic:
obtain ⟨_, _, ⟨⟩, hx⟩ := hf x

Goal state after:
X Y✝ : Type u
f : X ⟶ Y✝
hf : ∀ (x : Y✝), ∃ Y g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
x : (fun X ↦ X) Y✝
Y : Type u
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ ∃ a, (ConcreteCategory.hom f) a = x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ V ≤ U

Tactic:
rwa [preimage_image_eq] at e

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)

Tactic:
have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
this :
  IsIso
    (((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
        TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y) ≫
      inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : s ∈ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x)
⊢ s ∈
    Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))

Tactic:
simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
⊢ ∀ (i_1 : ↥(unop V)), (CommRingCat.Hom.hom (F.germ (unop V) ↑i_1 ⋯)) ((CommRingCat.Hom.hom (F.map i)) s) ∈ S ↑i_1
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      ((toBasicOpenₗ R M s) (LocalizedModule.mk f ⟨(fun x ↦ s ^ x) n, ⋯⟩)) =
    ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen s))))) (s ^ n))
      (const f (↑⟨(fun x ↦ s ^ x) n, ⋯⟩) (basicOpen s) ⋯)

Tactic:
dsimp [toBasicOpenₗ]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ s ^ n •
      (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
          (toOpenₗ R M (basicOpen s)) ⋯)
        (LocalizedModule.mk f ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯