harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_mkArray {f : α → Option β} (w : stop = n

Proof state:
case h
α : Type u_1
β : Type u_2
stop n : Nat
a : α
f : α → Option β
w : autoParam (stop = n) _auto✝
⊢ (match f a with
    | none => []
    | some b => List.replicate n b) =
    (match f a with
      | none => #[]
      | some b => mkArray n b).toList

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
stop n : Nat
a : α
f : α → Option β
w : autoParam (stop = n) _auto✝
⊢ (filterMap f (mkArray n a) 0 stop).toList =
    (match f a with
      | none => #[]
      | some b => mkArray n b).toList

Tactic:
simp only [w, size_mkArray, toList_filterMap', toList_mkArray, List.filterMap_replicate]

Result:
case h
α : Type u_1
β : Type u_2
stop n : Nat
a : α
f : α → Option β
w : autoParam (stop = n) _auto✝
⊢ (match f a with
    | none => []
    | some b => List.replicate n b) =
    (match f a with
      | none => #[]
      | some b => mkArray n b).toList

Proof state:
α : Type u_1
β : Type u_2
stop n : Nat
a : α
f : α → Option β
w : autoParam (stop = n) _auto✝
⊢ filterMap f (mkArray n a) 0 stop =
    match f a with
    | none => #[]
    | some b => mkArray n b

Tactic:
apply Array.ext'

Result:
case h
α : Type u_1
β : Type u_2
stop n : Nat
a : α
f : α → Option β
w : autoParam (stop = n) _auto✝
⊢ (filterMap f (mkArray n a) 0 stop).toList =
    (match f a with
      | none => #[]
      | some b => mkArray n b).toList
-- Mathlib/Algebra/Homology/Localization.lean
lemma mem_quasiIso_iff {X Y : HomotopyCategory C c} (f : X ⟶ Y) :
    quasiIso C c f ↔ ∀ (n : ι), IsIso ((homologyFunctor _ _ n).map f)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
X Y : HomotopyCategory C c
f : X ⟶ Y
⊢ quasiIso C c f ↔ ∀ (n : ι), IsIso ((homologyFunctor C c n).map f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_add_eq_sub_pi {x y : ℝ} (h : 1 < x * y) (hx : x < 0) :
    arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Proof state:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
rw [show _ / _ = -((x + y) / (1 - x * y)) by ring, ← neg_inj] at k

Result:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Proof state:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
simp only [arctan_neg, neg_add, neg_neg, ← sub_eq_add_neg _ π] at k

Result:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Proof state:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ (-x + -y) / (1 - -x * -y) = -((x + y) / (1 - x * y))

Tactic:
ring

Result:
no goals

Proof state:
x y : ℝ
h : 1 < x * y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
rw [← neg_mul_neg] at h

Result:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Proof state:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
have k := arctan_add_eq_add_pi h (neg_pos.mpr hx)

Result:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Proof state:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
exact k

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
@[to_additive]
lemma _root_.Finite.of_finite_mulAction_orbitRel_quotient [Finite G] [Finite Ω] : Finite α

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ ∀ (g : Ω), Finite ↑g.orbit

Tactic:
intro g

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
g : Ω
⊢ Finite ↑g.orbit

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
this : ∀ (g : Ω), Finite ↑g.orbit
⊢ Finite ((ω : Ω) × ↑ω.orbit)

Tactic:
exact Finite.instSigma

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite α

Tactic:
rw [(selfEquivSigmaOrbits' G _).finite_iff]

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite ((ω : Ω) × ↑ω.orbit)

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
g : Ω
⊢ Finite ↑g.orbit

Tactic:
induction g using Quotient.inductionOn'

Result:
case h
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
a✝ : α
⊢ Finite ↑(orbitRel.Quotient.orbit (Quotient.mk'' a✝))

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite ((ω : Ω) × ↑ω.orbit)

Tactic:
have : ∀ g : Ω, Finite g.orbit := by
  intro g
  induction g using Quotient.inductionOn'
  simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
this : ∀ (g : Ω), Finite ↑g.orbit
⊢ Finite ((ω : Ω) × ↑ω.orbit)

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
a✝ : α
⊢ Finite ↑(orbitRel.Quotient.orbit (Quotient.mk'' a✝))

Tactic:
simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_neg :
    mpullback I I' f (-V) = - mpullback I I' f V

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (-V) = -mpullback I I' f V

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullback I I' f (-V) x = (-mpullback I I' f V) x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
x : M
⊢ mpullback I I' f (-V) x = (-mpullback I I' f V) x

Tactic:
simp [mpullback_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_preΨ₄_ne_zero (h : (2 : R) ≠ 0) : W.preΨ₄.coeff 6 ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ W.preΨ₄.coeff 6 ≠ 0

Tactic:
rwa [coeff_preΨ₄]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_rev (x y : V) : o.oangle y x = -o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle y x = -o.oangle x y

Tactic:
simp only [oangle, o.kahler_swap y x, Complex.arg_conj_coe_angle]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_empty : IsCaratheodory m ∅

Proof state:
α : Type u
m : OuterMeasure α
⊢ m.IsCaratheodory ∅

Tactic:
simp [IsCaratheodory, m.empty, diff_empty]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_lt_base_pow_length {b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) :
    ofDigits b l < b ^ l.length

Proof state:
case succ.succ
l : List ℕ
b : ℕ
hb : 1 < b + 1 + 1
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Tactic:
simp_all

Result:
case succ.succ
l : List ℕ
b : ℕ
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Proof state:
b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
⊢ ofDigits b l < b ^ l.length

Tactic:
rcases b with (_ | _ | b) <;> try simp_all

Result:
case succ.succ
l : List ℕ
b : ℕ
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Proof state:
case succ.succ
l : List ℕ
b : ℕ
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Tactic:
exact ofDigits_lt_base_pow_length' hl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
@[simp]
lemma coprodMk_inr (x : Y) :
    coprodMk X Y (.inr x) = (coprod.inr : Y ⟶ X ⨿ Y).base x

Proof state:
case e_a.e_a
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.right } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr

Tactic:
exact coprodComparison_inr Scheme.forgetToTop

Result:
no goals

Proof state:
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ (coprodMk X Y) (Sum.inr x) = (ConcreteCategory.hom coprod.inr.base) x

Tactic:
show ((TopCat.binaryCofan X Y).inr ≫
  (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
    Scheme.forgetToTop.map coprod.inr x

Result:
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inr)) x

Proof state:
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inr)) x

Tactic:
congr 2

Result:
case e_a.e_a
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr

Proof state:
case e_a.e_a
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Result:
case e_a.e_a
X Y : Scheme
x : ↑↑Y.toPresheafedSpace
⊢ colimit.ι (pair ↑X.toPresheafedSpace ↑Y.toPresheafedSpace) { as := WalkingPair.right } ≫
      (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_one {x : 𝕜} :
    iteratedDerivWithin 1 f s x = derivWithin f s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : 𝓝[s \ {x}] x = ⊥
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Tactic:
simp [derivWithin_zero_of_isolated hxs, iteratedDerivWithin, iteratedFDerivWithin,
  fderivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x

Tactic:
simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply hxs, derivWithin]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_div_mul_cancel {a : Ordinal} (ha : a ≠ 0) (b c) : a * b / (a * c) = b / c

Proof state:
case h.e'_2
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = (a * b + 0) / (a * c)

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = b / c

Tactic:
convert mul_add_div_mul (Ordinal.pos_iff_ne_zero.2 ha) b c using 1

Result:
case h.e'_2
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = (a * b + 0) / (a * c)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_left_inj [IsDomain R] {x : R} (hx : x ≠ 0) :
    I * span {x} = J * span {x} ↔ I = J

Proof state:
R : Type u
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ I * span {x} = J * span {x} ↔ I = J

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_left_mono hx]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.iInter [Countable ι'] {s : ι' → Set X} (hs : ∀ i, IsGδ (s i)) :
    IsGδ (⋂ i, s i)

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
⊢ IsGδ (⋂ i, s i)

Tactic:
obtain rfl : s = fun i => ⋂₀ T i := funext hTs

Result:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ i, (fun i => ⋂₀ T i) i)

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
⊢ IsGδ (⋂ i, s i)

Tactic:
choose T hTo hTc hTs using hs

Result:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
⊢ IsGδ (⋂ i, s i)

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ i, (fun i => ⋂₀ T i) i)

Tactic:
refine ⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩

Result:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ t ∈ ⋃ i, T i, IsOpen t

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ t ∈ ⋃ i, T i, IsOpen t

Tactic:
simpa [@forall_swap ι'] using hTo

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGE_of_eq_eq {o : Ordering} : o = .eq → o.isGE

Proof state:
⊢ eq.isGE = true

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordering
⊢ o = eq → o.isGE = true

Tactic:
rintro rfl

Result:
⊢ eq.isGE = true
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem spanSingleton_div_spanSingleton (x y : K) :
    spanSingleton R₁⁰ x / spanSingleton R₁⁰ y = spanSingleton R₁⁰ (x / y)

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : K
⊢ spanSingleton R₁⁰ x / spanSingleton R₁⁰ y = spanSingleton R₁⁰ (x / y)

Tactic:
rw [div_spanSingleton, mul_comm, spanSingleton_mul_spanSingleton, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem map_contract {p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : R[X]} :
    (q.contract p).map f = (q.map f).contract p := ext fun n ↦ by
  simp only [coeff_map, coeff_contract hp]

Proof state:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
hp : p ≠ 0
f : R →+* S
q : R[X]
n : ℕ
⊢ (map f (contract p q)).coeff n = (contract p (map f q)).coeff n

Tactic:
simp only [coeff_map, coeff_contract hp]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem sublist_insertionSort {l c : List α} (hr : c.Pairwise r) (hc : c <+ l) :
    c <+ insertionSort r l

Proof state:
case cons.cons₂
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr

Result:
case cons.cons₂.intro
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr✝ : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
hr : ∀ a' ∈ l₁✝, r head✝ a'
hp : Pairwise r l₁✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Proof state:
case cons.cons₂.intro
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr✝ : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
hr : ∀ a' ∈ l₁✝, r head✝ a'
hp : Pairwise r l₁✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
exact cons_sublist_orderedInsert (ih hp h) hr

Result:
no goals

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
hr : Pairwise r c
hc : c <+ []
⊢ c <+ insertionSort r []

Tactic:
simp_all only [sublist_nil, insertionSort, Sublist.refl]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
⊢ c <+ insertionSort r l

Tactic:
induction l generalizing c with
| nil         => simp_all only [sublist_nil, insertionSort, Sublist.refl]
| cons _ _ ih =>
  cases hc with
  | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
  | cons₂ _ h =>
    obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
    exact cons_sublist_orderedInsert (ih hp h) hr

Result:
no goals

Proof state:
case cons.cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hr : Pairwise r c
h : c <+ tail✝
⊢ c <+ insertionSort r (head✝ :: tail✝)

Tactic:
exact ih hr h |>.trans (sublist_orderedInsert ..)

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hr : Pairwise r c
hc : c <+ head✝ :: tail✝
⊢ c <+ insertionSort r (head✝ :: tail✝)

Tactic:
cases hc with
| cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
| cons₂ _ h =>
  obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
  exact cons_sublist_orderedInsert (ih hp h) hr

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem comp_snoc {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n → α) (y : α) :
    g ∘ snoc q y = snoc (g ∘ q) (g y)

Proof state:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
⊢ g ∘ snoc q y = snoc (g ∘ q) (g y)

Tactic:
ext j

Result:
case h
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Proof state:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
rw [eq_last_of_not_lt h]

Result:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)

Proof state:
case h
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
by_cases h : j.val < n

Result:
case pos
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Proof state:
case pos
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
simp [h, snoc, castSucc_castLT]

Result:
no goals

Proof state:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_of_sub_pos {a b : Int} (h : 0 < a - b) : b < a

Proof state:
a b : Int
h✝ : 0 < a - b
h : 0 + b < a - b + b
⊢ b < a

Tactic:
rwa [Int.sub_add_cancel, Int.zero_add] at h

Result:
no goals

Proof state:
a b : Int
h : 0 < a - b
⊢ b < a

Tactic:
have h := Int.add_lt_add_right h b

Result:
a b : Int
h✝ : 0 < a - b
h : 0 + b < a - b + b
⊢ b < a