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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), a • f z = a • ∮ (z : ℂ) in C(c, R), f z

Tactic:
simp only [circleIntegral, ← smul_comm a (_ : ℂ) (_ : E), intervalIntegral.integral_smul]

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

Goal state before:
pp: case convert_1
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0

pp: case convert_2
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ -1 ≤ n → 0 ≤ n + 1

Tactic:
exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Goal state before:
pp: ⊢ MeasurePreserving (⇑measurableEquivPi) volume volume

Tactic:
convert! (measurableEquivPi.symm.measurable.measurePreserving volume).symm

Goal state after:
case e'_6
⊢ volume = Measure.map (⇑measurableEquivPi.symm) volume
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ ∫ (z : α × β), (B (f z.1)) (g z.2) ∂μ.prod ν = (B (∫ (x : α), f x ∂μ)) (∫ (y : β), g y ∂ν)

Tactic:
have : Integrable (fun z ↦ B (f z.1) (g z.2)) (μ.prod ν) :=
    hf.op_fst_snd (by fun_prop) ⟨‖B‖, B.le_opNorm₂⟩ hg

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun z ↦ (B (f z.1)) (g z.2)) (μ.prod ν)
⊢ ∫ (z : α × β), (B (f z.1)) (g z.2) ∂μ.prod ν = (B (∫ (x : α), f x ∂μ)) (∫ (y : β), g y ∂ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
mF : MeasurableSpace F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : Measure E
inst✝² : IsProbabilityMeasure μ
ν : Measure F
inst✝¹ : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst✝ : CompleteSpace G
hLμ : Integrable (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ
hLν : Integrable (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν
⊢ ∫ (p : E × F), L p ∂μ.prod ν =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν

Tactic:
by
  simp_rw [← L.comp_inl_add_comp_inr]
  replace hLμ := ((memLp_one_iff_integrable.mpr hLμ).comp_fst ν).integrable le_rfl
  replace hLν := ((memLp_one_iff_integrable.mpr hLν).comp_snd μ).integrable le_rfl
  rw [integral_add hLμ hLν, integral_prod _ hLμ, integral_prod _ hLν]
  simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map (fun x ↦ s ^ x.card • x.prod) (powersetCard n m)).sum = (map (fun x ↦ s • x) m).esymm n

Tactic:
· simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]

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✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
rw [support_esymm'']
  congr
  funext
  exact Finsupp.support_single _ one_ne_zero

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (C a * X))) l atTop

Tactic:
clear hd p

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (C a * X))) l atTop
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p * X))) l atTop

Tactic:
clear hd p

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p * X))) l atTop
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) l atTop

Tactic:
clear hd p

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) l atTop
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Function.Bijective ⇑(galActionHom p ℂ)

Tactic:
have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree := by
    simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
    rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
    · exact IsAlgClosed.splits _
    · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)

Goal state after:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
⊢ Function.Bijective ⇑(galActionHom p ℂ)
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 : R
hx0 : v x ≠ 0
hx1 : v x ≠ 1
⊢ v.restrict x ≠ 0

Tactic:
by simp [hx0]

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

Goal state before:
pp: case refine_2
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : (restrict₀ (ofClass v.restrict)) k = ↑x
⊢ (hom v) (v.restrict k) < γ

Tactic:
· convert! h
    simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]
    congr 1
    exact (embedding_restrict₀ k).symm

Goal state after:
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
⊢ Subsingleton (ofClass v).ValueGroup₀ˣ ∨ ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (hom' v) (v.restrict x) < γ

Tactic:
by
  simp only [ne_eq, or_iff_not_imp_left, not_subsingleton_iff_nontrivial]
  exact fun H ↦ (rankOne_of_nontrivial v H).exists_val_lt

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ (∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0) → w ≤ φ.lexOrder

Tactic:
· intro h
    rw [← not_lt]
    intro h'
    have hφ : φ ≠ 0 := by
      rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
      exact ne_top_of_lt h'
    obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ
    refine coeff_ne_zero_of_lexOrder hd.symm (h d ?_)
    rwa [← hd]

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

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

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder (d := u), zero_mul]

Goal state after:
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
⊢ ↑(toLex u) < φ.lexOrder
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
simp [hg]

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

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

Tactic:
add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.addXYZ P Q = -(Q y ^ 2 * P z) • P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
          P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
            0)

Tactic:
by
  rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
      (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
    0

Tactic:
by linear_combination (norm := ring1) u ^ 2 * hP'.right.right

Goal state after:
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
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (eval (⇑f ∘ P)) (W'.map f).polynomial = 0

Tactic:
map_polynomial,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (eval (⇑f ∘ P)) ((MvPolynomial.map f) W'.polynomial) = 0
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) ≤ TopologicalSpace.induced ULift.down c.pt.str

Tactic:
induced_of_isLimit _ hc,

Goal state after:
case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) ≤
    TopologicalSpace.induced ULift.down
      (⨅ j, TopologicalSpace.induced (⇑(ConcreteCategory.hom (c.π.app j))) (K.obj j).str)
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1
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
⊢ (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))

Tactic:
refine ofHom <| ContinuousMap.liftCover (fun i ↦ Set.range (𝒰.f i)) ?_ ?_ ?_

Goal state after:
case refine_1.refine_1
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
⊢ (i : 𝒰.I₀) → C(↑(Set.range ⇑(ConcreteCategory.hom (𝒰.f i))), ↑X)

case refine_1.refine_2
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
⊢ ∀ (i j : 𝒰.I₀) (x : ↑Y) (hxi : x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
    (hxj : x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.f j))),
    (?refine_1.refine_1 i) ⟨x, hxi⟩ = (?refine_1.refine_1 j) ⟨x, hxj⟩

case refine_1.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
⊢ ∀ (x : ↑Y), ∃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.f i)) ∈ nhds x
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case e'_5
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) = ⊥

Tactic:
eq_bot_iff

Goal state after:
case e'_5
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) ≤ ⊥
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_2
X : TopCat
E : precoverage.ZeroHypercover X
⊢ Presieve.map uliftFunctor E.presieve₀ ∈ isOpenEmbedding.precoverage.coverings (uliftFunctor.obj X)

Tactic:
· simp only [Presieve.map_ofArrows, MorphismProperty.ofArrows_mem_precoverage,
      isOpenEmbedding_iff]
    intro i
    exact (isOpenEmbedding_f_zeroHypercover _ _).uliftMap

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallySmooth
hg : g.FormallySmooth
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.FormallySmooth R S
algebraizeInst✝ : Algebra.FormallySmooth S T
⊢ (g.comp f).FormallySmooth

Tactic:
exact Algebra.FormallySmooth.comp R S T

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✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
this :
  LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[Localization.AtPrime p.asIdeal] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
exact ⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))

Tactic:
let P' : Extension R S := { Ring := P, σ := _, algebraMap_σ := Function.surjInv_eq h₁ }
  rw [Algebra.FormallySmooth.iff_injective_lTensor_residueField P' h₂]
  rw [P'.cotangentComplexBaseChange_eq_lTensor_cotangentComplex (ResidueField S)]
  refine .trans ?_ ((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _
    Ω[P'.Ring⁄R]).comp_injective _).symm
  exact (((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _ P'.ker).symm ≪≫ₗ
    P'.cotangentEquiv.baseChange (A := _)).injective_comp _).symm

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
inst✝ : Algebra.IsPushout R S A B
⊢ IsScalarTower S B (S ⊗[R] Ω[A⁄R])

Tactic:
by
  apply IsScalarTower.of_algebraMap_smul
  intro r x
  change (Algebra.pushoutDesc B (Algebra.lsmul R (A := S) S (S ⊗[R] Ω[A⁄R]))
    (Algebra.lsmul R (A := A) _ _) (LinearMap.ext <| smul_comm · ·)
      (algebraMap S B r)) • x = r • x
  simp only [Algebra.pushoutDesc_left, Module.End.smul_def, Algebra.lsmul_coe]

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
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) 1 = 0

Tactic:
← (algebraMap A B).map_one

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
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) 1) = 0
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

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

Tactic:
simp [Submodule.smul_mem_smul hr Submodule.mem_top]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
h : Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map f I)).comp f)
⊢ Function.Surjective ⇑f

Tactic:
let _ := f.toAlgebra

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
h : Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map f I)).comp f)
x✝ : Algebra R S := f.toAlgebra
⊢ Function.Surjective ⇑f
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
hy : f y ∈ Submodule.span R (Set.range (v ∘ a))
⊢ s (f y) = 0

Tactic:
revert hy

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
⊢ f y ∈ Submodule.span R (Set.range (v ∘ a)) → s (f y) = 0