harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ioc_add_zsmul : ⋃ n : ℤ, Ioc (a + n • p) (a + (n + 1) • p) = univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p

Proof state:
case h.e'_4
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p

Tactic:
abel

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + toIocDiv hp a b • p + p

Tactic:
convert sub_le_iff_le_add.mp hr using 1

Result:
case h.e'_4
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Ioc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Result:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + toIocDiv hp a b • p + p
-- Mathlib/Analysis/Convex/Strong.lean
nonrec lemma StrongConvexOn.strictConvexOn (hf : StrongConvexOn s m f) (hm : 0 < m) :
    StrictConvexOn ℝ s f := hf.strictConvexOn fun r hr ↦ by positivity

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
m : ℝ
hf : StrongConvexOn s m f
hm : 0 < m
r : ℝ
hr : r ≠ 0
⊢ 0 < m / 2 * r ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma pullbackWithin_eq_of_not_isInvertible {f : E → F} {x : E}
    (h : ¬(fderivWithin 𝕜 f s x).IsInvertible) (V : F → F) :
    pullbackWithin 𝕜 f V s x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ¬(fderivWithin 𝕜 f s x).IsInvertible
V : F → F
⊢ pullbackWithin 𝕜 f V s x = 0

Tactic:
simp [pullbackWithin, h]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcdB_zero_right {s : ℕ} (h : s ≠ 0) : gcdB s 0 = 0

Proof state:
s : ℕ
h : s ≠ 0
⊢ (s.xgcdAux 1 0 0 0 1).2.2 = 0

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Result:
case intro
s : ℕ
h : s.succ ≠ 0
⊢ (s.succ.xgcdAux 1 0 0 0 1).2.2 = 0

Proof state:
case intro
s : ℕ
h : s.succ ≠ 0
⊢ (s.succ.xgcdAux 1 0 0 0 1).2.2 = 0

Tactic:
rw [xgcdAux]

Result:
case intro
s : ℕ
h : s.succ ≠ 0
⊢ ((0 % s.succ).xgcdAux (0 - ↑(0 / s.succ) * 1) (1 - ↑(0 / s.succ) * 0) s.succ 1 0).2.2 = 0

Proof state:
s : ℕ
h : s ≠ 0
⊢ s.gcdB 0 = 0

Tactic:
unfold gcdB xgcd

Result:
s : ℕ
h : s ≠ 0
⊢ (s.xgcdAux 1 0 0 0 1).2.2 = 0

Proof state:
case intro
s : ℕ
h : s.succ ≠ 0
⊢ ((0 % s.succ).xgcdAux (0 - ↑(0 / s.succ) * 1) (1 - ↑(0 / s.succ) * 0) s.succ 1 0).2.2 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiff.one_of_succ (h : ContDiff 𝕜 (n + 1) f) : ContDiff 𝕜 1 f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
h : ContDiff 𝕜 (n + 1) f
⊢ ContDiff 𝕜 1 f

Tactic:
apply h.of_le le_add_self

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem le_coe_iff : x ≤ b ↔ ∃ a : α, x = a ∧ a ≤ b

Proof state:
α : Type u_1
b : α
inst✝ : LE α
x : WithTop α
⊢ x ≤ ↑b ↔ ∃ a, x = ↑a ∧ a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
lemma innerRegularWRT_isClosed_isOpen [R1Space α] [OpensMeasurableSpace α] [h : InnerRegular μ] :
    InnerRegularWRT μ IsClosed IsOpen

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Tactic:
rcases h.innerRegular hU.measurableSet r hr with ⟨K, KU, K_comp, hK⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
K : Set α
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
⊢ μ.InnerRegularWRT IsClosed IsOpen

Tactic:
intro U hU r hr

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
K : Set α
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Tactic:
exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure,
  hK.trans_le (measure_mono subset_closure)⟩

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
@[simp]
lemma trunc_one_left (p : R⟦X⟧) : trunc (R := R) 1 p = .C (coeff R 0 p)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
⊢ trunc 1 p = Polynomial.C ((coeff R 0) p)

Tactic:
ext i

Result:
case a
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i : ℕ
⊢ (trunc 1 p).coeff i = (Polynomial.C ((coeff R 0) p)).coeff i

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i : ℕ
⊢ (trunc 1 p).coeff i = (Polynomial.C ((coeff R 0) p)).coeff i

Tactic:
simp +contextual [coeff_trunc, Polynomial.coeff_C]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_mul (g : F[X]) :
    (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Proof state:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]

Result:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f.aroots (AlgebraicClosure F)).toFinset ∪ (g.aroots (AlgebraicClosure F)).toFinset).card ≤
    (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card

Proof state:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f.aroots (AlgebraicClosure F)).toFinset ∪ (g.aroots (AlgebraicClosure F)).toFinset).card ≤
    (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
exact Finset.card_union_le _ _

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
classical
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
exact Finset.card_union_le _ _

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
simp only [h, natSepDegree_zero, zero_le]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f g : F[X]
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
by_cases h : f * g = 0

Result:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem smul_eq_map [MulSemiringAction M R] (m : M) :
    HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Proof state:
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ m • (monomial n) r = map (MulSemiringAction.toRingHom M R m) ((monomial n) r)

Tactic:
rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply]

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
r : R[X]
⊢ m • r = map (MulSemiringAction.toRingHom M R m) r

Tactic:
exact DFunLike.congr_fun this r

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom

Tactic:
ext n r : 2

Result:
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ ((DistribMulAction.toAddMonoidHom R[X] m).comp (monomial n).toAddMonoidHom) r =
    ((mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom.comp (monomial n).toAddMonoidHom) r

Proof state:
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ ((DistribMulAction.toAddMonoidHom R[X] m).comp (monomial n).toAddMonoidHom) r =
    ((mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom.comp (monomial n).toAddMonoidHom) r

Tactic:
change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r)

Result:
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ m • (monomial n) r = map (MulSemiringAction.toRingHom M R m) ((monomial n) r)

Proof state:
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Tactic:
suffices DistribMulAction.toAddMonoidHom R[X] m =
    (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom by
  ext1 r
  exact DFunLike.congr_fun this r

Result:
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom

Proof state:
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Tactic:
ext1 r

Result:
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
r : R[X]
⊢ m • r = map (MulSemiringAction.toRingHom M R m) r
-- Mathlib/Data/PNat/Basic.lean
theorem sub_coe (a b : ℕ+) : ((a - b : ℕ+) : ℕ) = ite (b < a) (a - b : ℕ) 1

Proof state:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1

Tactic:
rfl

Result:
no goals

Proof state:
a b : ℕ+
⊢ ↑(↑a - ↑b).toPNat' = if b < a then ↑a - ↑b else 1

Tactic:
split_ifs with h

Result:
case pos
a b : ℕ+
h : b < a
⊢ ↑(↑a - ↑b).toPNat' = ↑a - ↑b

case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Proof state:
a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1

Tactic:
change (toPNat' _ : ℕ) = ite _ _ _

Result:
a b : ℕ+
⊢ ↑(↑a - ↑b).toPNat' = if b < a then ↑a - ↑b else 1

Proof state:
case pos
a b : ℕ+
h : b < a
⊢ ↑(↑a - ↑b).toPNat' = ↑a - ↑b

Tactic:
exact toPNat'_coe (tsub_pos_of_lt h)

Result:
no goals

Proof state:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Tactic:
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]

Result:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_add : sin (x + y) = sin x * cos y + cos x * sin y

Proof state:
x y : ℂ
⊢ sin (x + y) = sin x * cos y + cos x * sin y

Tactic:
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, add_mul, add_mul, mul_right_comm, ← sinh_mul_I,
  mul_assoc, ← sinh_mul_I, ← cosh_mul_I, ← cosh_mul_I, sinh_add]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomialY (P : Fin 3 → R) :
    eval P W'.polynomialY = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C 2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2) =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2

Tactic:
rw [polynomialY_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C 2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2) =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2
-- Mathlib/GroupTheory/Index.lean
theorem index_inf_ne_zero (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
rw [← relindex_top_right] at hH hK ⊢

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relindex ⊤ ≠ 0
hK : K.relindex ⊤ ≠ 0
⊢ (H ⊓ K).relindex ⊤ ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relindex ⊤ ≠ 0
hK : K.relindex ⊤ ≠ 0
⊢ (H ⊓ K).relindex ⊤ ≠ 0

Tactic:
exact relindex_inf_ne_zero hH hK

Result:
no goals
-- Mathlib/Data/Sigma/Order.lean
theorem lt_def [∀ i, LT (α i)] {a b : Σi, α i} : a < b ↔ ∃ h : a.1 = b.1, h.rec a.2 < b.2

Proof state:
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < b.snd) → ⟨i, a⟩ < b

Tactic:
obtain ⟨j, b⟩ := b

Result:
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < ⟨j, b⟩.snd) → ⟨i, a⟩ < ⟨j, b⟩

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b

Tactic:
obtain ⟨i, a⟩ := a

Result:
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < b.snd) → ⟨i, a⟩ < b

Proof state:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd

Tactic:
rintro ⟨i, a, b, h⟩

Result:
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b ↔ ∃ h, h ▸ a.snd < b.snd

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b

Proof state:
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd
⊢ ⟨i, a⟩ < ⟨i, b⟩

Tactic:
exact lt.fiber _ _ _ h

Result:
no goals

Proof state:
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd < ⟨j, b⟩.snd) → ⟨i, a⟩ < ⟨j, b⟩

Tactic:
rintro ⟨rfl : i = j, h⟩

Result:
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd
⊢ ⟨i, a⟩ < ⟨i, b⟩

Proof state:
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd

Tactic:
exact ⟨rfl, h⟩

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.union {s₁ s₂ : Set α} (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂)
    (h₁ : TendstoLocallyUniformlyOn F f p s₁) (h₂ : TendstoLocallyUniformlyOn F f p s₂) :
    TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)

Tactic:
rw [← sUnion_pair]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})

Tactic:
refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_ <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem order_mul {Γ} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R]
    [NoZeroDivisors R] {x y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) :
    (x * y).order = x.order + y.order

Proof state:
case a.h
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ x.leadingCoeff * y.leadingCoeff ≠ 0

Tactic:
exact mul_ne_zero (leadingCoeff_ne_iff.mpr hx) (leadingCoeff_ne_iff.mpr hy)

Result:
no goals

Proof state:
case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).order ≤ x.order + y.order

Tactic:
apply order_le_of_coeff_ne_zero

Result:
case a.h
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Proof state:
case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support

Result:
no goals

Proof state:
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).order = x.order + y.order

Tactic:
apply le_antisymm

Result:
case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).order ≤ x.order + y.order

case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ x.order + y.order ≤ (x * y).order

Proof state:
case a.h
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
rw [coeff_mul_order_add_order x y]

Result:
case a.h
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ x.leadingCoeff * y.leadingCoeff ≠ 0

Proof state:
case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ x.order + y.order ≤ (x * y).order

Tactic:
rw [order_of_ne hx, order_of_ne hy, order_of_ne (mul_ne_zero hx hy), ← Set.IsWF.min_add]

Result:
case a
R : Type u_3
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.congr (hf : HasFPowerSeriesOnBall f p x r)
    (hg : EqOn f g (EMetric.ball x r)) : HasFPowerSeriesOnBall g p x r :=
  { r_le := hf.r_le
    r_pos := hf.r_pos
    hasSum := fun {y} hy => by
      convert hf.hasSum hy using 1
      apply hg.symm
      simpa [edist_eq_enorm_sub] using hy }

Proof state:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (EMetric.ball x r)
y : E
hy : y ∈ EMetric.ball 0 r
⊢ g (x + y) = f (x + y)

Tactic:
apply hg.symm

Result:
case h.e'_6.a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (EMetric.ball x r)
y : E
hy : y ∈ EMetric.ball 0 r
⊢ x + y ∈ EMetric.ball x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (EMetric.ball x r)
y : E
hy : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x => y) (g (x + y))

Tactic:
convert hf.hasSum hy using 1

Result:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (EMetric.ball x r)
y : E
hy : y ∈ EMetric.ball 0 r
⊢ g (x + y) = f (x + y)

Proof state:
case h.e'_6.a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (EMetric.ball x r)
y : E
hy : y ∈ EMetric.ball 0 r
⊢ x + y ∈ EMetric.ball x r

Tactic:
simpa [edist_eq_enorm_sub] using hy

Result:
no goals