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

Goal state before:
pp: case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *
    exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi

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

Goal state before:
pp: case refine_4
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
hx : x ∈ interior (Set.Icc a.1 b.1) ×ˢ interior (Set.Icc a.2 b.2) \ s
⊢ ∀ (i : Fin (1 + 1)), HasFDerivAt (![f, g] i) (![f', g'] i x) x

Tactic:
interior_Icc,

Goal state after:
case refine_4
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
hx : x ∈ Set.Ioo a.1 b.1 ×ˢ interior (Set.Icc a.2 b.2) \ s
⊢ ∀ (i : Fin (1 + 1)), HasFDerivAt (![f, g] i) (![f', g'] i x) x
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
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 : ℝ
⊢ ∀ (y : ℚ), y.num • 1 < 0 → ↑y = x → x ≤ 0

Tactic:
intro y

Goal state after:
case a
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 : ℝ
y : ℚ
⊢ y.num • 1 < 0 → ↑y = x → x ≤ 0
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∉ ball x r, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ

Tactic:
intro y

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
⊢ y ∉ ball x r → ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε, 0 < ε ∧ ball x_1 ε ⊆ closedBall x r

Tactic:
intro y

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
⊢ y ∈ closedBall x r → ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ IsOpen (closedBall x r)

Tactic:
rw [isOpen_iff]
    simp only [gt_iff_lt]
    intro y hy
    cases closedBall_eq_or_disjoint x y r with
    | inl hd =>
      use r
      simp [h, hd, ball_subset_closedBall]
    | inr hd =>
      simp [closedBall_eq_of_mem hy, h.not_gt] at hd

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r)

Tactic:
cases lt_or_gt_of_ne hr with
  | inl h =>
    simp [closedBall_eq_empty.mpr h]
  | inr h =>
    rw [isOpen_iff]
    simp only [gt_iff_lt]
    intro y hy
    cases closedBall_eq_or_disjoint x y r with
    | inl hd =>
      use r
      simp [h, hd, ball_subset_closedBall]
    | inr hd =>
      simp [closedBall_eq_of_mem hy, h.not_gt] at hd

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
x : K
hx : x ≠ 0
hxy : (RankLeOne.hom' valuation) (valuation.restrict x) < ⟨ε, ⋯⟩
⊢ {x_1 | valuation.restrict x_1 < ↑(Units.mk0 (valuation.restrict x) ⋯)} ⊆ U

Tactic:
intro y

Goal state after:
case h
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
x : K
hx : x ≠ 0
hxy : (RankLeOne.hom' valuation) (valuation.restrict x) < ⟨ε, ⋯⟩
y : K
⊢ y ∈ {x_1 | valuation.restrict x_1 < ↑(Units.mk0 (valuation.restrict x) ⋯)} → y ∈ U
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ ‖f a‖₊ ≠ ‖f j‖₊

Tactic:
apply hs

Goal state after:
case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ∈ ↑(Finset.cons a s ha)

case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ j ∈ ↑(Finset.cons a s ha)

case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ≠ j
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ → IsUnit (constantCoeff φ)

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ

Tactic:
· exact IsUnit.map _

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case inl
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x ≤ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
use x⁻¹
      simp only [toNormedField.one_lt_norm_iff, map_inv₀, one_lt_inv₀ (zero_lt_iff.mpr hx.1),
          lt_of_le_of_ne h hx.2]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Tactic:
have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by
    apply Ideal.finite_factors
    simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite
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
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
h_dense : DenseRange ⇑Φ
⊢ closure ↑Φ.range = Set.univ

Tactic:
exact h_dense.closure_range

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: 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
⊢ (ConcreteCategory.hom
          (Equalizer.Presieve.Arrows.firstMap F X c.inj ≫
            Pi.π (fun ij ↦ F.obj (op (Limits.pullback (c.inj ij.1) (c.inj ij.2)))) (i, j))).toFun
      a =
    (ConcreteCategory.hom
          (Equalizer.Presieve.Arrows.secondMap F X c.inj ≫
            Pi.π (fun ij ↦ F.obj (op (Limits.pullback (c.inj ij.1) (c.inj ij.2)))) (i, j))).toFun
      a

Tactic:
simp only [Equalizer.Presieve.Arrows.firstMap, limit.lift_π, Fan.mk_π_app,
    TypeCat.Fun.toFun_apply, comp_apply, Equalizer.Presieve.Arrows.secondMap]

Goal state after:
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
⊢ (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)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case e'_3
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ W'⁄B = (W'⁄A).map f.toRingHom

Tactic:
rw [AlgHom.toRingHom_eq_coe, map_baseChange]

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

Goal state before:
pp: X Y : TopCat
⊢ ∀ (E : precoverage.ZeroHypercover Y), Presieve.IsSheafFor (yoneda.obj X) E.presieve₀

Tactic:
𝒰

Goal state after:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
⊢ Presieve.IsSheafFor (yoneda.obj X) 𝒰.presieve₀
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := ⋯
⊢ Sieve (colimit F)

Tactic:
exact Sieve.ofArrows _ (colimit.ι F)

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

Goal state before:
pp: case ofLocalizationSpanTarget
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

pp: case ofLocalizationSpan
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

pp: case StableUnderCompositionWithLocalizationAwayTarget
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
· exact ofLocalizationSpanTarget

Goal state after:
case ofLocalizationSpan
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

case StableUnderCompositionWithLocalizationAwayTarget
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
x : B
hx : x ∈ RingHom.ker (Ideal.Quotient.mk J)
⊢ x ∈ J

Tactic:
simpa using! hx

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ 1 ⊗ₜ[R] 0 = 0

Tactic:
TensorProduct.tmul_zero

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ 0 = 0
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
a b : AdicCauchySequence I M
⊢ ⟨fun n ↦ f (↑(a + b) n), ⋯⟩ = ⟨fun n ↦ f (↑a n), ⋯⟩ + ⟨fun n ↦ f (↑b n), ⋯⟩

Tactic:
ext n; 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
r : R
a : AdicCauchySequence I M
⊢ ⟨fun n ↦ f (↑(r • a) n), ⋯⟩ = (RingHom.id R) r • ⟨fun n ↦ f (↑a n), ⋯⟩

Tactic:
ext n; 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
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ Function.Surjective ⇑(map I f)

Tactic:
intro y

Goal state after:
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
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
⊢ ∃ a, (map I f) a = y
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
inst✝¹ : IsPrecomplete I M
inst✝ : IsHausdorff I N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ Function.Surjective ⇑f

Tactic:
intro y

Goal state after:
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
inst✝¹ : IsPrecomplete I M
inst✝ : IsHausdorff I N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
⊢ ∃ a, f a = y
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
⊢ r • 0 = 0

Tactic:
ext n; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
x y : AdicCompletion I M
⊢ r • (x + y) = r • x + r • y

Tactic:
ext n; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
⊢ 0 • x = 0

Tactic:
ext n; simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

Goal state after:
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
P : Presentation 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₀
⊢ Ideal.span (Set.range (relationOfHasCoeffs R₀)) ≤ RingHom.ker (MvPolynomial.aeval P.val)

Tactic:
Ideal.span_le

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation 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₀
⊢ Set.range (relationOfHasCoeffs R₀) ⊆ ↑(RingHom.ker (MvPolynomial.aeval P.val))
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
P : Presentation 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₀
⊢ Ideal.span (Set.range P.relation) ≤
    RingHom.ker
      ((TensorProduct.map (AlgHom.id R R)
            (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
        ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)

Tactic:
Ideal.span_le

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation 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₀
⊢ Set.range P.relation ⊆
    ↑(RingHom.ker
        ((TensorProduct.map (AlgHom.id R R)
              (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
          ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm))
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).Etale ↔ Algebra.Etale R S

Tactic:
by
  rw [RingHom.Etale, toAlgebra_algebraMap]

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by
  rw [eq_formallyUnramified_and_smooth]
  exact FormallyUnramified.isStableUnderBaseChange.and Smooth.isStableUnderBaseChange

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K

Tactic:
rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
⊢ Algebra.IsIntegral (↥⊤) K
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyClosed (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsClosed
    (⇑(pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)) ''
      ⇑(pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
            (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯) ⁻¹'
        s)

Tactic:
exact p.isClosedMap _ (hs.preimage r.continuous)

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ (∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y) →
    ∀ (z : S), ∃ x_1 ∈ R[x], (algebraMap S L) x_1 = y * (algebraMap S L) z

Tactic:
rintro ⟨y, hy, rfl⟩ z
      exact ⟨_, hy z, map_mul _ _ _⟩

Goal state after: