mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
← hderiv,

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
⊢ -∫ (x : ℝ) in b..a, deriv f x = f b - f a

Tactic:
integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm,

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
⊢ -(f a - f b) = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : ℝ → E
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc t (t + T) → liftIoc T t f ↑x = f x

Tactic:
refine .of_forall fun x hx ↦ ?_

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : ℝ → E
x : ℝ
hx : x ∈ uIoc t (t + T)
⊢ liftIoc T t f ↑x = f x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ + ∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ ≤
    ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ (_t : ℝ) in Icc a b, δ ∂μ

Tactic:
gcongr with x hx x hx
      · exact (hf.uncurry_left _).norm.integrableOn_Icc
      · exact continuous_const.integrableOn_Icc
      · exact nullMeasurableSet_Icc
      · calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
        _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
        _ ≤ M + δ := by
            gcongr
            · apply hM
              change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
              apply mem_image_of_mem
              simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
              exact h'δ hx
            · exact le_of_lt (hv _ hp _ (h'δ hx))
        _ ≤ M + 1 := by linarith
      · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
      · exact continuous_const.integrableOn_Icc
      · exact nullMeasurableSet_Icc
      · exact le_of_lt (hv _ hp _ hx)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
⊢ ∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
let π : G' → G' ⧸ Γ' := QuotientAddGroup.mk
  have meas_π : Measurable π := continuous_quotient_mk'.measurable
  have H₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) :=
    QuotientAddGroup.automorphize_smul_left f g
  calc ∫ (x : G'), g (π x) * f x ∂μ' =
    ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
  have H₁ : Integrable ((g ∘ π) * f) μ' := by
    have : AEStronglyMeasurable (fun (x : G') ↦ g (x : (G' ⧸ Γ'))) μ' :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
    refine Integrable.essSup_smul f_ℒ_1 this ?_
    have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
    rw [← essSup_comp_quotientAddGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
  have H₂ : AEStronglyMeasurable (QuotientAddGroup.automorphize ((g ∘ π) * f)) μ_𝓕 := by
    simp_rw [H₀]
    exact hg.mul F_ae_measurable
  apply QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ.prod ν)
x : α
⊢ ‖∫ (y : β), f (x, y) ∂ν‖ ≤ ‖∫ (y : β), ‖f (x, y)‖ ∂ν‖

Tactic:
grw [norm_integral_le_integral_norm]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ.prod ν)
x : α
⊢ ∫ (a : β), ‖f (x, a)‖ ∂ν ≤ ‖∫ (y : β), ‖f (x, y)‖ ∂ν‖
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
rcases comp_eq_zero_iff.mp h₂ with h | h

Goal state after:
case pos.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : p₂ = 0
⊢ P (p₁ * p₂)

case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : (minpoly F α).natDegree = p.natDegree
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Tactic:
by
    let _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
    rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]

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

Goal state before:
pp: case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ ‖(map f p).coeff i‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
coeff_eq_zero_of_natDegree_lt hi,

Goal state after:
case inr.inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : (map f p).natDegree < i
⊢ ‖0‖ ≤ B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔
    m •
        (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
              (fun h ↦
                (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 })
                  h)
              (instDecidableEqNat den 0)).num •
          1 <
      den • x

Tactic:
conv in den • x => rw [hden, mul_comm, ← smul_smul]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔
    m •
        (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
              (fun h ↦
                (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 })
                  h)
              (instDecidableEqNat den 0)).num •
          1 <
      m •
        (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
              (fun h ↦
                (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 })
                  h)
              (instDecidableEqNat den 0)).den •
          x
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
use ne
    unfold lexOrder
    simp only [dif_neg hφ]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
by_cases hf : f.weightedOrder w < ⊤

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : ¬weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : IsDedekindDomain R
inst✝¹ : IsFractionRing R K
v✝ : HeightOneSpectrum R
inst✝ : NumberField K
v : FinitePlace K
x : K
⊢ v (-x) = v x

Tactic:
simp [coe_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).j = j

Tactic:
by_cases h3 : (3 : F) = 0
    · have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
      simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]
      linear_combination 576 * h3
    · have := Fact.mk (Ne.isUnit h3)
      simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      (2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0 ↔
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)

Tactic:
Iff.comm,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 ↔
        2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : i = j
⊢ (ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)

Tactic:
rw [hi, Mono.right_cancellation _ _ pullback.condition]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: ⊢ PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
by
  refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
  rw [nonempty_isLimit_iff_eq_induced]
  · refine le_antisymm ?_ ?_
    · rw [le_iInf_iff]
      rintro j s ⟨t, ht, rfl⟩
      refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
      apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
      apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht
    · change _ ≤ TopologicalSpace.induced _ _
      rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]
      rintro i s ⟨-, ⟨t, ht, rfl⟩, rfl⟩
      refine .basic _ ?_
      rw [Set.mem_iUnion]
      exact ⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩
  · exact isLimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
⊢ (aeval ((Ideal.Quotient.mk I) x)) (minpoly K pb.gen) = 0

Tactic:
hx,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
⊢ (aeval (f pb.gen)) (minpoly K pb.gen) = 0
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁' =
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂'

Tactic:
· ext r
      rw [← sub_eq_zero]
      simp only [Ideal.Quotient.algebraMap_eq, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
        Function.comp_apply, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, f₁', f₂',
        AlgHom.comp_toLinearMap, AlgHom.ofLinearMap_apply, LinearMap.coe_comp,
        LinearMap.coe_single, Function.comp_apply, AlgHom.toLinearMap_apply,
        Ideal.Quotient.mkₐ_eq_mk]
      exact Ideal.mem_map_of_mem (Ideal.Quotient.mk J') (hf (Pi.single x r))

Goal state after:
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝³ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝² : IsScalarTower R Sp Sq
this✝¹ : IsScalarTower Rp Sp Sq
this✝ : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : IsPushout R Rp S Sp
⊢ FinitePresentation Rp Sp

Tactic:
exact .equiv (Algebra.IsPushout.equiv R Rp S Sp)

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ (component (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) ((sumInv I M) x) = (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)
  rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ ((sumInv I M) x) j = (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)
  rfl

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case mul_X
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i✝ j : σ
p : MvPolynomial ι R
i : ι
hp :
  { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) p) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p
⊢ eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p *
      { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) (X i)) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p *
      eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) (X i)

Tactic:
simp [Presentation.toGenerators_comp, toPresentation_comp]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ IsUnit ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential).det

Tactic:
convert! P.jacobian_isUnit

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential).det = P.jacobian
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian

Tactic:
by
  classical
  let : Fintype σ := Fintype.ofFinite _
  rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (P x * Q z - Q x * P z) ^ 3 = 0

Tactic:
hx,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (Q x * P z - Q x * P z) ^ 3 = 0