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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace Y
inst✝² : CompactSpace Y
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMap.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMap.evalCLM ℝ y (f x) ∂μ :=
          (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖
⊢ ‖(y - x) • (L e (n e) m - f')‖ ≤ ‖y - x‖ * (12 * (1 / 2) ^ e)

Tactic:
rw [norm_smul]; gcongr; exact Lf' _ _ m_ge

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
simpa only [mul_comm c] using integral_comp_mul_right f hc

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ

Tactic:
let H := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), 0 x ≤ f x := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Icc (-ε) (0 + ε) ⊆ I

Tactic:
zero_add

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Icc (-ε) ε ⊆ I
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
wlog hT : 0 < T
  · rcases (not_lt.1 hT).eq_or_lt with h | h
    · tauto
    · have hnT : 0 < -T := neg_pos.mpr h
      nth_rw 1 [(by ring : t = (t + T) + (-T))] at h₂f
      apply this h₁f.neg hnT.ne' h₂f.symm _ _ hnT
  -- Replace [a₁, a₂] by [t - n₁ * T, t + n₂ * T], where n₁ and n₂ are natural numbers
  obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t - min a₁ a₂) / T)
  obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)
  have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
    rw [Set.uIcc_subset_uIcc_iff_le]
    constructor
    · calc min (t - n₁ * T) (t + n₂ * T)
      _ ≤ (t - n₁ * T) := by apply min_le_left
      _ ≤ min a₁ a₂ := by linarith [(div_le_iff₀ hT).1 hn₁]
    · calc max a₁ a₂
      _ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
      _ ≤ max (t - n₁ * T) (t + n₂ * T) := by apply le_max_right
  apply IntervalIntegrable.mono_set _ this
  -- Suffices to show integrability over shifted periods
  let a : ℕ → ℝ := fun n ↦ t + (n - n₁) * T
  rw [(by ring : t - n₁ * T = a 0), (by simp [a] : t + n₂ * T = a (n₁ + n₂))]
  apply IntervalIntegrable.trans_iterate
  -- Show integrability over a shifted period
  intro k hk
  convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) enorm_ne_top) using 1
  · funext x
    simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm
  · simp [a, Nat.cast_add]
    ring

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

Goal state before:
pp: c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (0 + 2 * π)

Tactic:
zero_add

Goal state after:
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ (n + 1) • ∫ (x : ℝ) in 0..T, f x = (n + 1) • ∫ (x : ℝ) in 0..0 + T, f x

Tactic:
zero_add

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

Goal state before:
pp: case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ n

Tactic:
← zpow_neg_one

Goal state after:
case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C * (2 * π)

Tactic:
mul_comm (R * C),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * (R * C)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
apply hasFiniteIntegral_congr

Goal state after:
case h₂
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ (fun x ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) =ᵐ[μ] fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν
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 ^ n • x) ∘ prod) (powersetCard n m)).sum = (map (fun x ↦ s ^ x.card • x.prod) (powersetCard n m)).sum

Tactic:
refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))
    rw [Function.comp_apply, (mem_powersetCard.1 hx).2]

Goal state after:
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 : ℕ
e : σ ≃ τ
⊢ (rename ⇑e) (hsymm σ R n) = hsymm τ R n

Tactic:
simp_rw [hsymm, map_sum, ← prod_hom', rename_X]

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x, (Multiset.map (fun x ↦ X (e x)) ↑x).prod = ∑ s, (Multiset.map X ↑s).prod
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: 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✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔
    Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
by
  rw [←
    LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero, ← Set.wellFoundedOn_range]
  classical
  refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
  · rintro ⟨_, x, rfl⟩
    simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_ofPred_eq, Set.mem_range,
      Function.comp_apply]
    intro hx
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
    exact ⟨y, by simp⟩
  · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
  · intro
    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_ofPred_eq,
      forall_exists_index]
    rintro x rfl
    simp [← Subtype.coe_le_coe, hv.map_le_one]
  · simp [Function.onFun]

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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
this : ↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } ∈ ratLt' (y - x)
⊢ 0 < ↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ }

Tactic:
by simp [← Rat.num_pos]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := (_ : Set X) ⊆ _), or_assoc]

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := (_ : Set X) ⊆ _), or_assoc]

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬valuation.restrict x = 0
⊢ False

Tactic:
← ne_eq,

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : valuation.restrict x ≠ 0
⊢ False
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_1
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✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
⊢ ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U

Tactic:
set δ : ℝ≥0 := hv.hom _ ε with hδ

Goal state after:
case refine_1
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✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (0, n).1 + (0, n).2 = n

Tactic:
zero_add

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (0, n).2 = n
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ (∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) +
      -∑ x ∈ (antidiagonal n).erase (0, n), if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) =
    0

Tactic:
←
        sub_eq_add_neg,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ (∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) -
      ∑ x ∈ (antidiagonal n).erase (0, n), if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) =
    0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
⊢ 1 ∈ R⁰

Tactic:
exact Submonoid.one_mem R⁰

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

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (x - y))) = ↑((RankOne.hom v) (v.restrict (-x + y)))

Tactic:
← v.restrict.map_neg,

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (-(x - y)))) = ↑((RankOne.hom v) (v.restrict (-x + y)))
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inl
σ : 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 < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ ¬f = 0

Tactic:
← ne_eq,

Goal state after:
case inl
σ : 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 < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ f ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inr
σ : 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 < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ ¬g = 0

Tactic:
← ne_eq,

Goal state after:
case inr
σ : 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 < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ g ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [inv_eq_zero.mpr h]
    simp only [map_mul, mul_eq_zero] at h
    -- we don't have `NoZeroDivisors (MvPowerSeries σ k)` yet,
    rcases h with h | h <;> simp [inv_eq_zero.mpr h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
j : R
⊢ (ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3

Tactic:
simp only [ofJNe0Or1728, c₄, b₂, b₄]

Goal state after:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ ((j - 1728) ^ 2 + 4 * 0) ^ 2 - 24 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) = j * (j - 1728) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
⊢ (ofJ j).IsElliptic

Tactic:
by
  by_cases h0 : j = 0
  · by_cases h3 : (3 : F) = 0
    · have : Fact <| IsUnit (2 : F) := ⟨.of_mul_eq_one 2 <| by linear_combination h3⟩
      rw [h0, ofJ_0_of_three_eq_zero h3]
      infer_instance
    · have := Fact.mk (Ne.isUnit h3)
      rw [h0, ofJ_0_of_three_ne_zero h3]
      infer_instance
  · by_cases h1728 : j = 1728
    · have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
      have := Fact.mk h2.isUnit
      rw [h1728, ofJ_1728_of_two_ne_zero h2]
      infer_instance
    · have := Fact.mk (Ne.isUnit h0)
      have := Fact.mk (sub_ne_zero.2 h1728).isUnit
      rw [ofJ_ne_0_ne_1728 j h0 h1728]
      infer_instance

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
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P y ^ 2 * Q z) • Q

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = 0 + toAffine W Q

Tactic:
zero_add

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = toAffine W Q
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ precoverage IsOpenImmersion ≤
    Precoverage.comap forgetToTop
        (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage) ⊓
      Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
precoverage

Goal state after:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ⊓ IsOpenImmersion.precoverage ≤
    Precoverage.comap forgetToTop
        (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage) ⊓
      Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case 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✝ : 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} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

Tactic:
suffices Ideal.Quotient.mk (Ideal.span {1 - e i}) (e i) = 1 by simp [ι, ← he', this]

Goal state after:
case 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✝ : 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' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ (Ideal.Quotient.mk (Ideal.span {1 - e i})) (e i) = 1
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.smul
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
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * s✝ • n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
| smul _ _ e =>

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x

Tactic:
apply induction_on I M x h

Goal state after: