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

Goal state before:

Tactic:
∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p q : F[X]
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ restrictDvd hpq = if hq : q = 0 then 1 else restrict p q.SplittingField

Tactic:
unfold restrictDvd
  congr

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) p).Splits
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩))

Tactic:
← AlgEquiv.restrictNormal_commutes

Goal state after:
case neg.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) p).Splits
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal g p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩))
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) q).Splits
key :
  x = (algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap q.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f q.SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    g ((algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩))

Tactic:
← AlgEquiv.restrictNormal_commutes

Goal state after:
case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) q).Splits
key :
  x = (algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap q.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f q.SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    (algebraMap q.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal g q.SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: S : Type u_4
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Algebra R S
n : ℕ
f : σ → S
⊢ ∑ x ∈ powersetCard n univ, ∏ x ∈ x, f x = (Multiset.map f univ.val).esymm n

Tactic:
esymm_map_val

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (esymm σ R n).degrees = univ.val

Tactic:
rw [degrees_def, support_esymm, sup_image, this]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (powersetCard n univ).sup val = univ.val
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ (rename ⇑e) (msymm σ R μ) = msymm τ R μ

Tactic:
by
  rw [msymm, map_sum]
  apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)
  intro
  rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]
  simp

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ z ∈ ball c ↑R \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ eball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n ↦ (cauchyPowerSeries f c (↑R) n) fun x ↦ w) (f (c + w))

Tactic:
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
      hs hw' hc hd]

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ z ∈ ball c ↑R \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ eball 0 ↑R
hw' : c + w ∈ ball c ↑R
⊢ HasSum (fun n ↦ (cauchyPowerSeries f c (↑R) n) fun x ↦ w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - (c + w))⁻¹ • f z)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

Tactic:
this,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ x ∈ range (s.card + 1), Polynomial.C (esymm σ R x) * Polynomial.X ^ (s.card - x)
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ IsPrincipalIdealRing O

Tactic:
this,

Goal state after:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ WfDvdMonoid O
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ (u + v).num • 1 < (u + v).den • (x + y)

Tactic:
refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_
    rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]

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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
this : ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
⊢ (u + v).num • 1 < (u + v).den • (x + y)

Tactic:
by
    refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_
    rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]

Goal state after:
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 : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
h' : x < 0
⊢ ∃ y < 0, x < ↑y

Tactic:
obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'

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 : ℝ
h : ∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x
h' : x < 0
y : ℚ
hxy : x < ↑y
hy : ↑y < 0
⊢ ∃ y < 0, x < ↑y
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_4
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
⊢ Nontrivial (ofClass v).ValueGroup₀ˣ → ∀ {γ : ℝ≥0}, ¬γ = 0 → ∃ x, ¬x = 0 ∧ (hom' v) (v.restrict x) < γ

Tactic:
exact fun H ↦ (rankOne_of_nontrivial v H).exists_val_lt

Goal state after:
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 : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
h' : x < 1
⊢ ∃ y < 1, x < ↑y

Tactic:
obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'

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 : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
h' : x < 1
y : ℚ
hxy : x < ↑y
hy : ↑y < 1
⊢ ∃ y < 1, x < ↑y
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_1.inr
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 | valuation.restrict x < ↑γ} ⊆ U

Tactic:
obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp hε)

Goal state after:
case refine_1.inr
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 | valuation.restrict x < ↑γ} ⊆ U
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
| X ^ f.order.toNat * f.divXPowOrder

Tactic:
this,

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
| X ^ ENat.toNat 0 * f.divXPowOrder
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 ↑x ≠ 1}.Finite

Tactic:
this,

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
⊢ {x_1 | x_1 ↑x < 1}.Finite
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: 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)

Tactic:
· exact (s.property r).symm

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
      nonsingular_neg_of_Z_ne_zero hP hPz]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m ↦ m • Q) u x * Q z = Q x * (fun m ↦ m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q x * Q z = Q x * (↑u * Q z)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m ↦ m • Q) u y * Q z = Q y * (fun m ↦ m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q y * Q z = Q y * (↑u * Q z)
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'.addY P (W'.neg P) = -W'.dblZ P

Tactic:
simp only [addY, addX_neg, negAddY_neg hP, addZ_neg, negY, fin3_def_ext, mul_zero, sub_zero]

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

Goal state before:
pp: case neg
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:
have := preservesTerminal_of_isSheaf_for_empty F hF hI
    apply_fun (F.mapIso ((hd hi).isoPullback).op ≪≫ F.mapIso (terminalIsoIsTerminal
      (terminalOpOfInitial initialIsInitial)).symm ≪≫ (PreservesTerminal.iso F)).hom using
      injective_of_mono _
    ext ⟨i⟩
    exact i.elim

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

Goal state before:
pp: case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
i : 𝒰.I₀
y : ↑(𝒰.X i)
this : (Hom.hom f) ((Hom.hom (𝒰.f i)) y) = (Hom.hom (x i)) y
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (𝒰.f i)) y) =
    (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
        (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)
      ((ConcreteCategory.hom (𝒰.f i)) y)

Tactic:
this,

Goal state after:
case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
i : 𝒰.I₀
y : ↑(𝒰.X i)
this : (Hom.hom f) ((Hom.hom (𝒰.f i)) y) = (Hom.hom (x i)) y
⊢ (Hom.hom (x i)) y =
    (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
        (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)
      ((ConcreteCategory.hom (𝒰.f i)) y)
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: case e'_1
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
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
have := IsLocalizedModule.iso p.asIdeal.primeCompl
      (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))

Goal state after:
case e'_1
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
this : LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.AtPrime p.asIdeal)
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
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
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R (Localization.Away 1)

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
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ ↑(PrimeSpectrum.basicOpen 1) ⊆ smoothLocus R A
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 (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) = 1

Tactic:
rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
        Ideal.Quotient.eq_zero_iff_mem]

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
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case intro.mpr
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
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
let iso : B ≃ₐ[R] ∀ i, B ⧸ Ideal.span {1 - e i} :=
      { __ := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R _
        __ := Equiv.ofBijective _ he.bijective_pi }

Goal state after:
case intro.mpr
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
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g