mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case h
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 α
⊢ (minpoly F α).natDegree = p.natDegree

Tactic:
suffices minpoly F α ∣ p by
    have key := (minpoly.irreducible hα).dvd_symm p_irr this
    apply le_antisymm
    · exact natDegree_le_of_dvd this p_irr.ne_zero
    · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)

Goal state after:
case h
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 α
⊢ minpoly F α ∣ p
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (fun x ↦ eval x p) (cocompact R) (cocompact R)

Tactic:
rw [← Metric.cobounded_eq_cocompact, ← tendsto_norm_atTop_iff_cobounded]
    exact p.tendsto_norm_atTop h tendsto_norm_cobounded_atTop

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case mpr
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
⊢ (aeval z) p = 0 ∧ z.im = 0 → ∃ a, (aeval a) p = 0 ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z

Tactic:
· rintro ⟨hz1, hz2⟩
      have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
        ext
        · rfl
        · rw [hz2]; rfl
      exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, map_zero]), key⟩

Goal state after:
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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
⊢ -x < -x - x

Tactic:
simpa using hneg

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : (ofClass v).ValueGroup₀
hx : (hom v) x = 0
h_lt : 0 < x
hs : 0 < 0
⊢ False

Tactic:
exact hs.false

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : (ofClass v).ValueGroup₀
h : x = 0
⊢ (hom v) x = 0

Tactic:
by rw [h, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ unit v ≠ 1

Tactic:
Ne,

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ ¬unit v = 1
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    ∫ (x : ℝ) in Set.Icc a₁ b₁, ∫ (y : ℝ) in Set.Icc a₂ b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1)

Tactic:
by
      simp only [intervalIntegral.integral_of_le, h₁, h₂,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
rw [tprod_eq_one_of_not_multipliable h, norm_one']
    by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
    · exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)
    · rw [Real.iSup_of_not_bddAbove h_bd]

Goal state after:
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
⊢ φ.lexOrder = ⊤ ↔ φ = 0

Tactic:
unfold lexOrder
  split_ifs with h
  · simp only [h]
  · simp only [h, WithTop.coe_ne_top]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (coeff n) (inv.aux a φ) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (inv.aux a φ) else 0

Tactic:
by
  rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]
  simp only [Finsupp.single_eq_zero]
  split_ifs; · rfl
  congr 1
  symm
  apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())
  · aesop
  · aesop
  · aesop
  · aesop
  · rintro ⟨i, j⟩ _hij
    obtain H | H := le_or_gt n j
    · aesop
    rw [if_pos H, if_pos]
    · rfl
    refine ⟨?_, fun hh ↦ H.not_ge ?_⟩
    · rintro ⟨⟩
      simpa [Finsupp.single_eq_same] using le_of_lt H
    · simpa [Finsupp.single_eq_same] using hh ()

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ↑f.Unit_of_divided_by_X_pow_order = f.divXPowOrder

Tactic:
by simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ mk v₁ ≠ mk v₂

Tactic:
DFunLike.ne_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f✝ : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
⊢ Presieve.IsSeparatedFor F (Presieve.ofArrows (fun i ↦ pullback (𝒰.f i) f) fun x ↦ pullback.snd (𝒰.f x) f)

Tactic:
apply H₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
⊢ gi ≫ E.f i = gj ≫ E.f j → (ConcreteCategory.hom (F.map gi.op)) (s i) = (ConcreteCategory.hom (F.map gj.op)) (s j)

Tactic:
hgij

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
⊢ (ConcreteCategory.hom (F.map gi.op)) (s i) = (ConcreteCategory.hom (F.map gj.op)) (s j)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
by
  rcases h with ⟨u, rfl⟩
  exact toAffine_smul Q u.isUnit

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

Goal state before:
pp: case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ∀ (i : J✝),
    (uliftFunctor.mapCone c).pt.str ≤
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app i)))
        ((K ⋙ uliftFunctor).obj i).str

Tactic:
rintro j s ⟨t, ht, rfl⟩

Goal state after:
case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
j : J✝
t : Set ↑((K ⋙ uliftFunctor).obj j)
ht : IsOpen t
⊢ IsOpen (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)) ⁻¹' t)
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
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
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
have : FiniteDimensional K K⟮x, y⟯ := by
      apply IntermediateField.finiteDimensional_adjoin
      intro x _; exact (Algebra.IsSeparable.isSeparable K x).isIntegral

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
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
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this : FiniteDimensional K ↥K⟮x, y⟯
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
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
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
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : IntermediateField.adjoin K (⇑K⟮x, y⟯.val '' {⟨α, hα⟩}) = K⟮x, y⟯.val.fieldRange
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
simp only [IntermediateField.coe_val, Set.image_singleton,
      IntermediateField.fieldRange_val] at e

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
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
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : K⟮α⟯ = K⟮x, y⟯
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : IsSepClosed K
x : K
p : PrimeSpectrum K
⊢ (equivPiOfIsSepClosed K K) x p = x

Tactic:
let := Ideal.Quotient.field p.asIdeal
  dsimp [equivPiOfIsSepClosed]
  simp only [Equiv.piCongrLeft_symm_apply, AlgEquiv.piCongrRight_apply,
    IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal, IsArtinianRing.equivPi_apply]
  apply (AlgEquiv.ofBijective (ofId K (K ⧸ p.asIdeal))
    (IsSepClosed.algebraMap_bijective _ _)).injective
  simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
x : M
hx : x ∈ I • ⊤
⊢ x ∈ Submodule.comap f (I • ⊤)

Tactic:
refine Submodule.smul_induction_on hx (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
x✝¹ : M
hx : x✝¹ ∈ I • ⊤
r : R
hr : r ∈ I
x : M
x✝ : x ∈ ⊤
⊢ r • x ∈ Submodule.comap f (I • ⊤)

case refine_2
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
x✝ : M
hx✝ : x✝ ∈ I • ⊤
x y : M
hx : x ∈ Submodule.comap f (I • ⊤)
hy : y ∈ Submodule.comap f (I • ⊤)
⊢ x + y ∈ Submodule.comap f (I • ⊤)
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 ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M ∘ₗ sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) n = ↑(LinearMap.id ((mk I (⨁ (j : ι), M j)) f)) n

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe,
    Submodule.mkQ_apply]

Goal state after:
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 ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) f))) n = Submodule.Quotient.mk (↑f n)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.Surjective ⇑(evalOneₐ I)

Tactic:
dsimp [evalOneₐ]
  exact (Ideal.Quotient.factor_surjective (show I ^ 1 ≤ I by simp)).comp
    (AdicCompletion.surjective_evalₐ I 1)

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)
⊢ (ofTensorProductEquivOfFiniteNoetherian I M).symm ((ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)) =
    1 ⊗ₜ[R] x

Tactic:
LinearEquiv.symm_apply_apply

Goal state after:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)
⊢ 1 ⊗ₜ[R] x = 1 ⊗ₜ[R] x
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 σ
⊢ ((aeval P.val).mapMatrix P.jacobiMatrix).det = (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
P.algebraMap_eq

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 σ
⊢ ((aeval P.val).mapMatrix P.jacobiMatrix).det = ↑(aeval P.val) P.jacobiMatrix.det
Module: Mathlib.RingTheory.Smooth.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
w✝⁵ w✝⁴ : Type
w✝³ : Finite w✝⁴
left✝¹ : Finite w✝⁵
P : SubmersivePresentation R S w✝⁵ w✝⁴
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
Q : SubmersivePresentation S T w✝² w✝¹
⊢ ∃ ι σ, ∃ (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
exact ⟨_, _, _, inferInstance, ⟨Q.comp P⟩⟩

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

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
w✝⁷ w✝⁶ : Type
w✝⁵ : Finite w✝⁶
w✝⁴ : Finite w✝⁷
P : SubmersivePresentation R S w✝⁷ w✝⁶
hP : P.dimension = n
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
Q : SubmersivePresentation S T w✝³ w✝²
hQ : Q.dimension = m
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = m + n

Tactic:
refine ⟨_, _, _, inferInstance, Q.comp P, hP ▸ hQ ▸ ?_⟩

Goal state after:
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
w✝⁷ w✝⁶ : Type
w✝⁵ : Finite w✝⁶
w✝⁴ : Finite w✝⁷
P : SubmersivePresentation R S w✝⁷ w✝⁶
hP : P.dimension = n
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
Q : SubmersivePresentation S T w✝³ w✝²
hQ : Q.dimension = m
⊢ (Q.comp P).dimension = Q.dimension + P.dimension
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
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
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblY P / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblXYZ P = W.dblU P • ![0, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e

Tactic:
algebraize [e.toRingHom]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
algInst✝ : Algebra R S := e.toRingHom.toAlgebra
⊢ IsStandardSmoothOfRelativeDimension 0 ↑e
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t).IsHomogeneous 1

pp: case refine_2.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)

Tactic:
· rw [ht]
      exact D.hqhom i

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)