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

Goal state before:
pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ MeasurePreserving (⇑e) volume volume

pp: case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

pp: case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume

Tactic:
· exact (volume_preserving_funUnique (Fin 1) ℝ).symm _

Goal state after:
case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
| p.coeff k

Tactic:
rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
| (C p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod).coeff k
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
obtain ⟨a, -, b, -, habne, h⟩ :=
    Set.Infinite.exists_ne_map_eq_of_mapsTo (f := (x ^ · : ℕ → K)) Set.infinite_univ
      (fun a _ => mem_ofPred.mpr <|
        ⟨hxi.pow a, fun φ => by simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]⟩)
      (finite_of_norm_le K A (1 : ℝ))
  wlog hlt : b < a
  · exact this K A hx₀ hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)
  refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
  rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h
  refine h.resolve_right fun hp ↦ hx₀ (eq_zero_of_pow_eq_zero hp)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
ψ : K →+* ℂ
inst✝ : Algebra K L
φ : ComplexEmbedding.Extension L ψ
h : ¬IsReal ψ
⊢ (conjugate ↑φ).comp (algebraMap K L) ≠ ψ

Tactic:
by
  simp_all [ComplexEmbedding.isReal_iff, comp_eq]

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 Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
x : Multiplicative ℝ
⊢ NNReal.mk (2 ^ (↑x).log) ⋯ ≠ 0

Tactic:
simp only [ne_eq, NNReal.eq_iff, NNReal.coe_mk, NNReal.coe_zero]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
x : Multiplicative ℝ
⊢ ¬2 ^ (↑x).log = 0
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
⊢ x = 0

Tactic:
refine (eq_of_le_of_not_lt (zero_le (a := x)) fun h_lt ↦ ?_).symm
  have hs := strictMono v h_lt
  rw [map_zero, hx] at hs
  exact hs.false

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

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
calc
    map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2))
    _ = X ^ 2 - C (↑(2 * z.re) : ℂ) * X + C (‖z‖ ^ 2 : ℂ) := by simp
    _ = (X - C (conj z)) * (X - C z) := by
      rw [← add_conj, map_add, ← mul_conj', map_mul]
      ring

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
hxy : x < y
⊢ (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) y

Tactic:
(WithZero.map'_strictMono (MulEquiv.strictMono_symm (mulintEquivOfZPowersEqTop_strictMono
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)
    (Left.one_lt_inv_iff.mpr hv.generator'_lt_one)))).lt_iff_lt

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
hxy : x < y
⊢ x < y
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
⊢ (coeff d) φ = 0

Tactic:
rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩
    rw [hφ', WithTop.coe_lt_coe] at h
    by_contra h'
    exact WellFounded.not_lt_min _ (toLex '' φ.support) (Set.mem_image_equiv.mpr h') h

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
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
⊢ (coeff (u, v).1) φ * (coeff (u, v).2) ψ = 0

Tactic:
rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u = p ∧ v = q
⊢ (coeff (u, v).1) φ * (coeff (u, v).2) ψ = 0

case inr.inl
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u < p
⊢ (coeff (u, v).1) φ * (coeff (u, v).2) ψ = 0

case inr.inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
⊢ (coeff (u, v).1) φ * (coeff (u, v).2) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case inr.inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
⊢ ↑(toLex v) < ψ.lexOrder

Tactic:
rw [hq]

Goal state after:
case inr.inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
⊢ ↑(toLex v) < ↑(toLex q)
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_2
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this✝ : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
this : Nontrivial Γ₀ˣ
⊢ ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U

Tactic:
obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos

Goal state after:
case refine_2
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this✝ : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
this : Nontrivial Γ₀ˣ
u : (ofClass v).ValueGroup₀ˣ
hu : ↑((RankOne.hom v) ↑u) < r
⊢ ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
        | (a, b) => (single () a, single () b)).2
      PUnit.unit ≤
    (single () n) PUnit.unit

Tactic:
simpa [Finsupp.single_eq_same] using le_of_lt H

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
h : f = f.divXPowOrder
⊢ IsUnit f

Tactic:
rw [h]; exact isUnit_divided_by_X_pow_order hf

Goal state after:
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✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : K
⊢ ‖(embedding v) x‖ = ↑((toNNReal ⋯) ((valuation K v) x))

Tactic:
norm_embedding,

Goal state after:
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✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : K
⊢ (HeightOneSpectrum.adicAbv K v) x = ↑((toNNReal ⋯) ((valuation K v) x))
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✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ‖(embedding v) ((algebraMap R K) x)‖ *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Tactic:
norm_embedding,

Goal state after:
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✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ (adicAbv K v) ((algebraMap R K) x) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
⊢ (fun i ↦
      match i with
      | WalkingMulticospan.left i => s.val i
      | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j))) ∈
    I.multicospan.sections

Tactic:
rintro _ _ (_ | _ | r)

Goal state after:
case id
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
j✝ : WalkingMulticospan J
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.id j✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        j✝) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      j✝

case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] = -W'.dblZ P • ![0, 1, 0]

Tactic:
addX_neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] = -W'.dblZ P • ![0, 1, 0]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: 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
⊢ (W'⁄B).polynomialZ = (MvPolynomial.map ↑f) (W'⁄A).polynomialZ

Tactic:
rw [← map_polynomialZ, map_baseChange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
⊢ Sieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀

Tactic:
rw [Sieve.generate_le_iff]

Goal state after:
D : GlueData
⊢ Presieve.ofArrows D.openCover.X D.openCover.f ≤ { I₀ := D.J, X := D.U, f := D.ι }.sieve₀.arrows
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h,

Goal state after:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).dblXYZ (⇑f ∘ P) = ⇑f ∘ W.add P Q
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R S : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).Smooth

Tactic:
smooth_algebraMap

Goal state after:
R S : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Algebra.Smooth R S
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
· have := IsLocalizedModule.iso p.asIdeal.primeCompl
        (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
      have := this.extendScalarsOfIsLocalization
        p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
      exact ⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ Smooth R (Localization.Away f)

Tactic:
basicOpen_subset_smoothLocus_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ FormallySmooth R (Localization.Away f) ↔ Smooth R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : FinitePresentation R A
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst✝¹ } ∈ ↑(basicOpen f)
hf : ↑(basicOpen f) ⊆ smoothLocus R A
⊢ FormallySmooth R (Localization.Away f)

Tactic:
basicOpen_subset_smoothLocus_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : FinitePresentation R A
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst✝¹ } ∈ ↑(basicOpen f)
hf : FormallySmooth R (Localization.Away f)
⊢ FormallySmooth R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case g.map_one
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✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

Tactic:
change Ideal.Quotient.mk _ (Pi.single i 1) = 1

Goal state after:
case g.map_one
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✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) = 1
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
k : L
this✝² : Algebra.IsSeparable K ↥K⟮k⟯
this✝¹ : FiniteDimensional K ↥K⟮k⟯
this✝ : FormallyEtale K ↥K⟮k⟯
this : Function.Bijective (Ideal.Quotient.mkₐ K I).comp
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)

Tactic:
exact this.existsUnique _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.Surjective (⇑(Ideal.Quotient.factorₐ R ⋯) ∘ ⇑(evalₐ I 1))

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

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x : R
h : I ^ n • ⊤ ≤ I ^ n
⊢ (factor h) ((eval I S n) ((liftRingHom I f ⋯) x)) = (f n) x

Tactic:
simp [liftRingHom, eval]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x : R
⊢ (factor ⋯) ((eval I S n) ((liftRingHom I f ⋯) x)) = (f n) x

Tactic:
simp [liftRingHom, eval]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
⊢ (map I f) ((mk I M) (AdicCauchySequence.mk I M (fun n ↦ ↑(a n)) ⋯)) = (mk I N) b

Tactic:
· ext n
      suffices h : Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f (a n)) =
            Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (b (k + n)) by
        simp [h, AdicCauchySequence.mk_eq_mk (show n ≤ k + n by lia)]
      rw [Submodule.Quotient.eq]
      have hle : (I ^ (k + n) • ⊤ : Submodule R N) ≤ (I ^ n • ⊤ : Submodule R N) :=
        Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))
      exact hle (a n).property

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
ι' : 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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = (algebraMap Q.Ring T) Q.jacobiMatrix.det

Tactic:
AlgHom.map_det (aeval (Q.comp P).val),

Goal state after:
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 σ'
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁).det = (algebraMap Q.Ring T) Q.jacobiMatrix.det