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
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ Tendsto (fun n ↦ ∮ (z : ℂ) in C(c, R), f n z) l (𝓝 (∮ (z : ℂ) in C(c, R), g z))

Tactic:
apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
  · refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
    · rw [funext (deriv_circleMap _ _)]
      fun_prop
    · fun_prop
    · simp [hR, MapsTo]
  · rw [Metric.tendstoUniformlyOn_iff] at h ⊢
    simp only [dist_smul₀, deriv_circleMap, norm_mul, norm_I, norm_circleMap_zero,
      abs_of_nonneg hR, mul_one]
    intro ε hε
    rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩
    refine (h δ hδ₀).mono fun i hi x hx ↦ ?_
    grw [← hRδ, hi (circleMap c R x) (by simp [hR])]

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

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

Tactic:
simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x ↦ f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
hIoo : ⋃ k, Box.Ioo ((J k).face i) = Box.Ioo (I.face i)
Hid : Integrable (fun x ↦ f (i.insertNth d x) i) (volume.restrict (⋃ k, Box.Ioo ((J k).face i)))
⊢ Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Ioo ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in ⋃ k, Box.Ioo ((J k).face i), f (i.insertNth d x) i))

Tactic:
exact tendsto_setIntegral_of_monotone (fun k => ((J k).face i).measurableSet_Ioo)
      (Box.Ioo.monotone.comp ((Box.monotone_face i).comp J.monotone)) Hid

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε

Tactic:
have hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c} :=
    sdiff_subset_sdiff_right (singleton_subset_iff.2 <| mem_closedBall_self hr0.le)

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ ↑n.factorial * (R * (C / R ^ (n + 1))) = ↑n.factorial * C / R ^ n

Tactic:
by
      grind

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

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖e (deriv f c)‖

Tactic:
exact (UniformSpace.Completion.norm_coe _).symm

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

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
by
  set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
  have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
    e.hasFDerivAt.comp_hasDerivAt c
      (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
  calc
    ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
      rw [this.deriv]
      exact (UniformSpace.Completion.norm_coe _).symm
    _ ≤ C / R :=
      norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
        (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
this : Fact (map (algebraMap F q.SplittingField) p).Splits
⊢ Function.Surjective ⇑(restrictDvd hpq)

Tactic:
simpa only [restrictDvd_def, dif_neg hq] using! restrict_surjective _ _

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 x : Multiset R
hx : x ∈ powersetCard n m
⊢ ((fun x ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod

Tactic:
rw [Function.comp_apply, (mem_powersetCard.1 hx).2]

Goal state after:
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
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ * X).leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop

Tactic:
leadingCoeff_mul_X

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]
a✝ : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
⊢ a.card = b.card + c.card

Tactic:
have ha : ∀ z : ℂ, z ∈ a ↔ aeval z p = 0 := by
    intro z; rw [Set.mem_toFinset, mem_rootSet_of_ne hp]

Goal state after:
case neg.refine_2.refine_2.refine_2
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
⊢ a.card = b.card + c.card
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
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 : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) =
    ∑ i,
      ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e a i) x)))

Tactic:
by
      refine integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ ![f, g]
        ![f', g'] s hs a b hle ?_ (fun x hx => ?_) _ ?_ Hi
      · exact fun x y => (OrderIso.finTwoArrowIso ℝ).symm.le_iff_le
      · exact (volume_preserving_finTwoArrow ℝ).symm _
      · exact Fin.forall_fin_two.2 ⟨Hcf, Hcg⟩
      · rw [Icc_prod_eq, interior_prod_eq, interior_Icc, interior_Icc] at hx
        exact Fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩
      · intro x; rw [Fin.sum_univ_two]; rfl

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
⊢ ((u + v).num * ↑u.den * ↑v.den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)

Tactic:
Rat.add_num_den',

Goal state after:
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
⊢ ((u.num * ↑v.den + v.num * ↑u.den) * ↑(u + v).den) • 1 < ↑(u + v).den • (↑u.den * ↑v.den) • (x + y)
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
⊢ Nonempty v.RankOne ↔ MulArchimedean (ofClass v).ValueGroup₀

Tactic:
constructor
  · intro h
    obtain hv := Nonempty.some h
    exact MulArchimedean.comap hv.hom'.toMonoidHom hv.strictMono'
  · intro _
    obtain ⟨f, hf⟩ :=
      Archimedean.exists_orderAddMonoidHom_real_injective (Additive (ValueGroup₀ (.ofClass v))ˣ)
    let e := AddMonoidHom.toMultiplicativeRight (α := (ValueGroup₀ (.ofClass v))ˣ) (β := ℝ) f
    have he : StrictMono e := by
      simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
      -- toAdd_strictMono is already in an applied form, do defeq abuse instead
      exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)
    let rf : Multiplicative ℝ →* ℝ≥0ˣ := {
      toFun x := Units.mk0 (.mk ((2 : ℝ) ^ (log (M := ℝ) x)) (by positivity)) <| by
        simp only [ne_eq, NNReal.eq_iff, NNReal.coe_mk, NNReal.coe_zero]
        positivity
      map_one' := by ext; simp
      map_mul' _ _ := by ext; simp [Real.rpow_add]
      }
    have H : StrictMono (map' (rf.comp e)) := by
      refine map'_strictMono ?_
      intro a b h
      simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h
    exact ⟨{
      hom' := withZeroUnitsEquiv.toMonoidWithZeroHom.comp <| (map' (rf.comp e)).comp
        withZeroUnitsEquiv.symm.toMonoidWithZeroHom
      strictMono' := withZeroUnitsEquiv_strictMono.comp <| H.comp
        withZeroUnitsEquiv_symm_strictMono
    }⟩

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

Goal state before:
pp: case h3
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
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ((galActionHom p ℂ) conj').IsSwap

Tactic:
· rw [← Equiv.Perm.card_support_eq_two]
    apply Nat.add_left_cancel
    rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

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) < ⟨ε, ⋯⟩
y : K
hy : ↑(valuation y) < ↑(valuation x)
⊢ ‖y‖ < ε

Tactic:
apply lt_trans hy

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
hy : ↑(valuation y) < ↑(valuation x)
⊢ ↑(valuation x) < ε
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : constantCoeff ↑ψ = f (constantCoeff φ)
⊢ IsUnit φ

Tactic:
have : IsUnit (constantCoeff ψ.val) := isUnit_constantCoeff _ ψ.isUnit

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : constantCoeff ↑ψ = f (constantCoeff φ)
this : IsUnit (constantCoeff ↑ψ)
⊢ IsUnit φ
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
⊢ ∀ (x_1 y : 𝓤.I₀), pullback.fst (𝓤.f x_1) (𝓤.f y) ≫ x (𝓤.f x_1) ⋯ = pullback.snd (𝓤.f x_1) (𝓤.f y) ≫ x (𝓤.f y) ⋯

Tactic:
by
    intro i j
    apply hx
    exact Limits.pullback.condition

Goal state after:
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 := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Presieve.ofArrows F.obj (colimit.ι F) ≤ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows

Tactic:
rintro - - ⟨i⟩

Goal state after:
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 := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows (colimit.ι F i)
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 := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ 𝟙 (F.obj i) ≫ c.ι.app i = colimit.ι F i ≫ iso.inv

Tactic:
by simp [iso]

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Projective R
W : Projective F
x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝ + 0) = (toAffineAddEquiv W) x✝

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

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

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this : IsScalarTower R Rₓ Sₓ
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝¹ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this✝ : IsScalarTower R Rₓ Sₓ
this : Algebra.FormallyUnramified Rₓ Sₓ
⊢ Algebra.IsUnramifiedAt R x.asIdeal
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Subsingleton Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ FormallyEtale R A

Tactic:
Algebra.formallyEtale_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Subsingleton Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ Subsingleton Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = s • (D S (S ⊗[R] A)) (1 ⊗ₜ[R] a)

Tactic:
← Derivation.map_smul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (D S (S ⊗[R] A)) (s • 1 ⊗ₜ[R] a)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = s • (D S (A ⊗[R] S)) (a ⊗ₜ[R] 1)

Tactic:
← Derivation.map_smul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (D S (A ⊗[R] S)) (s • a ⊗ₜ[R] 1)
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 y : AdicCompletion I R
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I R hmn) ((↑x * ↑y) n✝) = (↑x * ↑y) m✝

Tactic:
by
    simp [x.property, y.property, transitionMap_map_mul I hmn]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ
      ↑(piEquivOfFintype I fun x ↦ R) ∘ₗ ofTensorProduct I (ι → R) =
    LinearMap.id

Tactic:
piEquivOfFintype_comp_ofTensorProduct_eq

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ
      ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) =
    LinearMap.id
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_1
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
⊢ map I 0 = 0

Tactic:
AdicCompletion.map_zero

Goal state after:
case refine_1
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
⊢ 0 = 0
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
exact ofTensorProduct_bijective_of_map_from_fin I M f hf

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f (m + 1 + 1)) = liftAdicCompletionAux I f (m + 1)

Tactic:
rw [liftAdicCompletionAux, ← DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ]
    ext
    simp

Goal state after: