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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
⊢ ∃ z, ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)

Tactic:
set c := mk _ (val_sub_ne_zero f hx y)

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
⊢ ∃ z, ↑z - x ∈ ball K c
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 (A.valuation (↑a * (↑b - 1))) (A.valuation (↑a - 1))

Tactic:
mul_sub_one,

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 (↑a * ↑b - ↑a)) (A.valuation (↑a - 1))
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: 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 : Quotient (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))
⊢ ∀ ⦃x_1 : FiniteElement K⦄,
    x_1 ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x} →
      ∀ ⦃y : FiniteElement K⦄,
        y ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x} →
          Set.Icc x_1 y ⊆ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x}

Tactic:
rintro x rfl y hy z ⟨hxz, hzy⟩

Goal state after:
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
hy : y ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {⟦x⟧}
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
⊢ z ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {⟦x⟧}
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝² : Field K
A✝ : ValuationSubring K
L : Type u_1
J : Type u_2
inst✝¹ : Field L
inst✝ : Field J
A : ValuationSubring L
f : K →+* L
k : K
⊢ k ∈ (Subring.comap f A.toSubring).carrier ∨ k⁻¹ ∈ (Subring.comap f A.toSubring).carrier

Tactic:
simp [ValuationSubring.mem_or_inv_mem]

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

Goal state before:
pp: 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 * x) ≤ mk (z * y)

Tactic:
rw [← map_zero mk] at hz

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 : mk 0 ≤ mk z
⊢ mk (z * x) ≤ mk (z * y)
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : UpperSet α
⊢ ⋃ a ∈ Set.Ici 1, a • ↑s ⊆ ↑s

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset

Goal state after:
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑((↑f).supSpanSingleton x (f.eval x) hx) ⟨a + c • x, ⋯⟩

Tactic:
LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
⊢ seed.baseEmbedding ≤ (↑f).supSpanSingleton x (f.eval x) hx

Tactic:
exact le_trans f.prop.baseEmbedding_le <| LinearPMap.left_le_sup _ _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ g.mirror * h

Tactic:
exact dvd_mul_left h g.mirror

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
| cons b l hb =>

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

Goal state before:
pp: R : Type u_2
inst✝ : Field R
p : R[X]
x : R
⊢ eval x p =
    (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 0) / (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 1)

Tactic:
by
  simp [toTupleMvPolynomial, eval_homogenize]

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

Goal state before:
pp: case add
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : ℕ[X]
ph : ∀ (n : ℕ), p.smeval ↑n = ↑(p.smeval n)
qh : ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
⊢ ∀ (n : ℕ), (p + q).smeval ↑n = ↑((p + q).smeval n)

Tactic:
intro n
    simp only [smeval_add, ph, qh, Nat.cast_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ Irreducible p ↔ p.roots = 0

Tactic:
hp.irreducible_iff_lt_natDegree_lt hp1

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.degree = 1

Tactic:
rw [← Nat.cast_one, Polynomial.degree_eq_iff_natDegree_eq_of_pos (by simp)]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.natDegree = 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
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
⊢ ∀ b ∈ s, ((r₁ b - r₂ b) * ∏ k ∈ s.erase b, g k).degree < (∏ i ∈ s, g i).degree

Tactic:
intro j hj
        rw [← Finset.mul_prod_erase s g hj, mul_comm (g j), (hg.2 j hj).degree_mul]
        refine (degree_mul_le (r₁ j - r₂ j) (∏ k ∈ s.erase j, g k)).trans_lt ?_
        have dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥ := by
          rw [degree_ne_bot]
          exact (monic_prod_of_monic _ g
            fun j hj => hg.2 j (Finset.mem_of_mem_erase hj)).ne_zero_of_polynomial_ne
            fun h : r₂ i - r₁ i = g i => lt_irrefl _ (h ▸ hdr)
        rw [add_comm, WithBot.add_lt_add_iff_left dnb]
        exact (degree_sub_le (r₁ j) (r₂ j)).trans_lt (max_lt (hr₁.2 j hj) (hr₂.2 j hj))

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

Goal state before:
pp: case mp
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ norm z = 0 → z = 0

Tactic:
intro hz
    rw [norm_def] at hz
    by_cases h : z.im = 0
    · simp [h] at hz
      aesop
    · exfalso
      rw [← pow_two, sub_eq_zero, ← eq_sub_iff_add_eq] at hz
      apply Hab.out (-z.re / z.im)
      grind

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.j = c₃ • q.i

Tactic:
rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]

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
h_group : inst₁.toAddGroup = inst₂.toAddGroup
⊢ inst₁ = inst₂

Tactic:
injection h_group with h_group

Goal state after:
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
h_group :
  { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, toZSMul := inst₁.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ } =
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, toZSMul := inst₂.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case succ
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 α α
f : CentroidHom α
a b : α
n : ℕ
ih :
  let __AddMonoidHom := f.toEnd ^ n;
  (↑(f.toEnd ^ n)).toFun (a * b) = (↑(f.toEnd ^ n)).toFun a * b
__AddMonoidHom✝ : α →+ α := f.toEnd ^ (n + 1)
⊢ (↑(f.toEnd * f.toEnd ^ n)).toFun (a * b) = (↑(f.toEnd * f.toEnd ^ n)).toFun a * b

Tactic:
exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
f : G →* A
⊢ (fun f ↦ (↑f).comp (of k G)) ((fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) f) = f

Tactic:
ext
    simp [liftNCAlgHom, liftNCRingHom]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
⊢ (fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) ((fun f ↦ (↑f).comp (of k G)) F) = F

Tactic:
ext
    simp [liftNCAlgHom, liftNCRingHom]

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

Goal state before:
pp: case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star b✝ * Star.star a✝¹) (Star.star c✝ * Star.star a✝¹)

Tactic:
exact Rel.mul_left h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
a a' : G
b : k
inst✝ : Decidable (a = a')
⊢ (single a b).coeff a' = if a = a' then b else 0

Tactic:
by
  simp [Finsupp.single_apply]

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

Goal state before:
pp: case mp.inl
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0

Tactic:
exact ⟨rfl, le_antisymm (le_zero _) h⟩

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
l : List R
⊢ trop l.sum = (map trop l).prod

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop l.prod = (map untrop l).sum

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

Tactic:
ext
  simp only [compHahnSeries_coeff, map_add, coeff_apply_apply, HahnSeries.coeff_add', Pi.add_apply]
  rw [← HahnSeries.coeff_add]

Goal state after:
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
F : J ⥤ PresheafedSpace C
j : J
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))

Tactic:
apply (opEquiv _ _).injective

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j : J
⊢ (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
      ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
          (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
      (𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
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
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op =
    ((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
          (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
      ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
          (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op

Tactic:
apply (opEquiv _ _).injective

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
⊢ (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
      ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
          (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op =
    (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
      (((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
            (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
              (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
        ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
            (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
              (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x = Hom.stalkMap f y ≫ X.presheaf.stalkSpecializes h

Tactic:
dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
  refine colimit.hom_ext fun j => ?_
  induction j with | op j => ?_
  dsimp
  simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app,
    whiskerRight_app, NatTrans.id_app, colimit.ι_pre, assoc,
    colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocone.precompose_obj_ι,
    Cocone.whisker_ι, NatTrans.comp_app]
  tauto

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))

Tactic:
convert! hx

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) =
    (ConcreteCategory.hom (X.presheaf.germ U x hxU)) f