harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma comp_sum_left {ι : Type*} [Countable ι] (κ : Kernel α β) (η : ι → Kernel β γ) :
    (Kernel.sum η) ∘ₖ κ = Kernel.sum (fun i ↦ (η i) ∘ₖ κ)

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∀ (i : ι), AEMeasurable (fun b => ((η i) b) s✝) (κ a✝)

Tactic:
exact fun _ ↦ (Kernel.measurable_coe _ hs).aemeasurable

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = ((Kernel.sum fun i => η i ∘ₖ κ) a✝) s✝

Tactic:
simp_rw [sum_apply, comp_apply' _ _ _ hs, sum_apply, Measure.sum_apply _ hs,
  comp_apply' _ _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), ∑' (i : ι), ((η i) b) s✝ ∂κ a✝ = ∑' (i : ι), ∫⁻ (b : β), ((η i) b) s✝ ∂κ a✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), ∑' (i : ι), ((η i) b) s✝ ∂κ a✝ = ∑' (i : ι), ∫⁻ (b : β), ((η i) b) s✝ ∂κ a✝

Tactic:
rw [lintegral_tsum]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∀ (i : ι), AEMeasurable (fun b => ((η i) b) s✝) (κ a✝)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
⊢ Kernel.sum η ∘ₖ κ = Kernel.sum fun i => η i ∘ₖ κ

Tactic:
ext _ _ hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = ((Kernel.sum fun i => η i ∘ₖ κ) a✝) s✝
-- Mathlib/Data/List/Basic.lean
theorem eq_cons_of_mem_head? {x : α} : ∀ {l : List α}, x ∈ l.head? → l = x :: tail l
  | [], h => (Option.not_mem_none _ h).elim
  | a :: l, h => by
    simp only [head?, Option.mem_def, Option.some_inj] at h
    exact h ▸ rfl

Proof state:
α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail

Tactic:
exact h ▸ rfl

Result:
no goals

Proof state:
α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail

Tactic:
simp only [head?, Option.mem_def, Option.some_inj] at h

Result:
α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail
-- Mathlib/Algebra/Regular/SMul.lean
theorem of_smul_eq_one (h : a • s = 1) : IsSMulRegular M s :=
  of_smul a
    (by
      rw [h]
      exact one M)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1

Tactic:
exact one M

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)

Tactic:
rw [h]

Result:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
-- Mathlib/CategoryTheory/Triangulated/Functor.lean
lemma isTriangulated_of_precomp
    [(F ⋙ G).IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] :
    G.IsTriangulated where
  map_distinguished T hT

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²² : Category.{u_4, u_1} C
inst✝²¹ : Category.{u_6, u_2} D
inst✝²⁰ : Category.{u_5, u_3} E
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁶ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁵ : G.CommShift ℤ
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasZeroObject D
inst✝¹² : HasZeroObject E
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : Preadditive E
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
inst✝³ : Pretriangulated E
inst✝² : (F ⋙ G).IsTriangulated
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
obtain ⟨T', hT', ⟨e⟩⟩ := F.mem_mapTriangle_essImage_of_distinguished T hT

Result:
case intro.intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²² : Category.{u_4, u_1} C
inst✝²¹ : Category.{u_6, u_2} D
inst✝²⁰ : Category.{u_5, u_3} E
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁶ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁵ : G.CommShift ℤ
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasZeroObject D
inst✝¹² : HasZeroObject E
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : Preadditive E
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
inst✝³ : Pretriangulated E
inst✝² : (F ⋙ G).IsTriangulated
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
T' : Triangle C
hT' : T' ∈ distinguishedTriangles
e : F.mapTriangle.obj T' ≅ T
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Proof state:
case intro.intro.intro
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²² : Category.{u_4, u_1} C
inst✝²¹ : Category.{u_6, u_2} D
inst✝²⁰ : Category.{u_5, u_3} E
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁶ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁵ : G.CommShift ℤ
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasZeroObject D
inst✝¹² : HasZeroObject E
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : Preadditive E
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
inst✝³ : Pretriangulated E
inst✝² : (F ⋙ G).IsTriangulated
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
T' : Triangle C
hT' : T' ∈ distinguishedTriangles
e : F.mapTriangle.obj T' ≅ T
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
exact isomorphic_distinguished _ ((F ⋙ G).map_distinguished T' hT') _
  (G.mapTriangle.mapIso e.symm ≪≫ (mapTriangleCompIso F G).symm.app _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : Vector α n} : lex l₁ l₂ = true ↔ l₁ < l₂

Proof state:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } < l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
        fun x1 x2 => decide (x1 < x2)) =
      true ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } < { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Vector α n
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ l₁ < l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } < l₂

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
        fun x1 x2 => decide (x1 < x2)) =
      true ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } < { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma Filter.tendsto_const_div_iff {G : Type*} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G]
    (b : G) {c : G} {f : α → G} {l : Filter α} :
    Tendsto (fun k : α ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)

Proof state:
α : Type u
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun k => b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩

Result:
α : Type u
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k => b / f k) l (𝓝 (b / c))
⊢ Tendsto f l (𝓝 c)

Proof state:
α : Type u
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k => b / f k) l (𝓝 (b / c))
⊢ Tendsto f l (𝓝 c)

Tactic:
convert h.const_div' b with k <;> rw [div_div_cancel]

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem natCast_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : Matrix m n α) :
    (a : Matrix l l α) ⊗ₖ B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => a • B) :=
  diagonal_kronecker _ _ |>.trans <| by
    congr! 2
    ext
    simp [(Nat.cast_commute a _).eq]

Proof state:
case h.e'_6.h.e'_7
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ (fun i => ↑a •> B) = fun x => a •> B

Tactic:
ext

Result:
case h.e'_6.h.e'_7.h.a
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
x✝ : l
i✝ : m
j✝ : n
⊢ (↑a •> B) i✝ j✝ = (a •> B) i✝ j✝

Proof state:
case h.e'_6.h.e'_7.h.a
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
x✝ : l
i✝ : m
j✝ : n
⊢ (↑a •> B) i✝ j✝ = (a •> B) i✝ j✝

Tactic:
simp [(Nat.cast_commute a _).eq]

Result:
no goals

Proof state:
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => ↑a •> B) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun x => a •> B)

Tactic:
congr! 2

Result:
case h.e'_6.h.e'_7
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ (fun i => ↑a •> B) = fun x => a •> B
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.isoCoproduct_inv {f : J → C} [HasBiproduct f] :
    (biproduct.isoCoproduct f).inv = Sigma.desc (biproduct.ι f) :=
  colimit.hom_ext fun j => by simp [biproduct.isoCoproduct]

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : Discrete J
⊢ colimit.ι (Discrete.functor f) j ≫ (isoCoproduct f).inv = colimit.ι (Discrete.functor f) j ≫ Sigma.desc (ι f)

Tactic:
simp [biproduct.isoCoproduct]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ioc_right (a : α) : ⋃ b, Ioc a b = Ioi a

Proof state:
α : Type v
inst✝ : Preorder α
a : α
⊢ ⋃ b, Ioc a b = Ioi a

Tactic:
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
@[simp, norm_cast]
lemma cast_inj : (m : α) = n ↔ m = n

Proof state:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem zero_geom_sum : ∀ {n}, ∑ i ∈ range n, (0 : α) ^ i = if n = 0 then 0 else 1
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    rw [geom_sum_succ']
    simp [zero_geom_sum]

Proof state:
α : Type u
inst✝ : Semiring α
⊢ ∑ i ∈ range 0, 0 ^ i = if 0 = 0 then 0 else 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ 0 ^ (n + 1) + ∑ i ∈ range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1

Tactic:
simp [zero_geom_sum]

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
⊢ ∑ i ∈ range 1, 0 ^ i = if 1 = 0 then 0 else 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i ∈ range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1

Tactic:
rw [geom_sum_succ']

Result:
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ 0 ^ (n + 1) + ∑ i ∈ range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem _root_.IsPGroup.isCyclic_of_isZGroup [IsZGroup G] {p : ℕ} [Fact p.Prime]
    {P : Subgroup G} (hP : IsPGroup p P) : IsCyclic P

Proof state:
case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : IsZGroup G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
hQ : P ≤ ↑Q
⊢ IsCyclic ↥P

Tactic:
exact Subgroup.isCyclic_of_le hQ

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : IsZGroup G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
⊢ IsCyclic ↥P

Tactic:
obtain ⟨Q, hQ⟩ := hP.exists_le_sylow

Result:
case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : IsZGroup G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
hQ : P ≤ ↑Q
⊢ IsCyclic ↥P
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_add_of_ne_zero {q r : ℚ} (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    (q + r : ℚ) = (q + r : α)

Proof state:
case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Tactic:
exact mul_ne_zero hq hr

Result:
no goals

Proof state:
case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
push_cast

Result:
case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
  (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]

Result:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_zero : W.Φ 0 = 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 0 = 1

Tactic:
rw [Φ, ΨSq_zero, mul_zero, zero_sub, zero_add, preΨ_one, one_mul, zero_sub, preΨ_neg, preΨ_one,
  neg_one_mul, neg_neg, if_pos Even.zero]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_assoc_symm (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
  Function.comp_def, Equiv.prodAssoc_apply]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem comap_nhds_eq (h : X ≃ₜ Y) (y : Y) : comap h (𝓝 y) = 𝓝 (h.symm y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)

Tactic:
rw [h.nhds_eq_comap, h.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
@[gcongr] lemma IsPrefix.drop (h : l₁ <+: l₂) (n : ℕ) : l₁.drop n <+: l₂.drop n

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂

Tactic:
apply take_prefix

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n l₁ <+: List.drop n l₂

Tactic:
rw [prefix_iff_eq_take.mp h, drop_take]

Result:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
-- Mathlib/LinearAlgebra/Dual.lean
theorem comap_eval_surjective : (Submodule.comap (eval K V)).Surjective

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Surjective (comap (eval K V))

Tactic:
apply Submodule.comap_surjective_of_injective

Result:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Injective ⇑(eval K V)

Proof state:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ ker (eval K V) = ⊥

Tactic:
exact eval_ker K V

Result:
no goals

Proof state:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Injective ⇑(eval K V)

Tactic:
rw [← LinearMap.ker_eq_bot]

Result:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ ker (eval K V) = ⊥
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.int_mul_eq_of_eq_zero [Ring α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (hi : f 0 = 0) : ∀ n : ℤ, f (n * c) = 0
  | (n : ℕ) => by rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
  | .negSucc n => by rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(Int.negSucc n) * c) = 0

Tactic:
rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0

Tactic:
rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) :
    (⋃ i, s i).Infinite :=
  fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype
    (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦ hs (by simpa using h_eq)

Proof state:
α : Type u
ι : Type u_1
inst✝ : Infinite ι
s : ι → Set α
hs : Injective s
hfin : (⋃ i, s i).Finite
i j : ι
h_eq : (fun i => ⟨s i, ⋯⟩) i = (fun i => ⟨s i, ⋯⟩) j
⊢ s i = s j

Tactic:
simpa using h_eq

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_characterModule_baer : Flat R M ↔ Baer R (CharacterModule M)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ Baer R (CharacterModule M)

Tactic:
rw [equiv_iff (N := ULift.{u} M) ULift.moduleEquiv.symm, iff_characterModule_injective,
  ← Baer.iff_injective, Baer.congr (CharacterModule.congr ULift.moduleEquiv)]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_emptyset {f : β → α} : ⨆ x ∈ (∅ : Set β), f x = ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ ∅, f x = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_top : (mkMetric (fun _ => ∞ : ℝ≥0∞ → ℝ≥0∞) : OuterMeasure X) = ⊤

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
⊢ (mkMetric fun x => ⊤) = ⊤

Tactic:
simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]

Result:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ⊤ ≤ ⨆ r, ⨆ (_ : r > 0), ⊤

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ⊤ ≤ ⨆ r, ⨆ (_ : r > 0), ⊤

Tactic:
rw [le_iSup_iff]

Result:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
b : OuterMeasure X
hb : ∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b
⊢ ⊤ ≤ b

Tactic:
simpa using hb ⊤

Result:
no goals

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b

Tactic:
intro b hb

Result:
X : Type u_2
inst✝ : EMetricSpace X
b : OuterMeasure X
hb : ∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b
⊢ ⊤ ≤ b
-- Mathlib/Data/Matroid/Closure.lean
lemma isClosed_iff_isFlat {F : Iic M.E} : M.subtypeClosure.IsClosed F ↔ M.IsFlat F

Proof state:
α : Type u_2
M : Matroid α
F : ↑(Iic M.E)
⊢ M.subtypeClosure.IsClosed F ↔ M.IsFlat ↑F

Tactic:
simp [subtypeClosure]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pred_lt_castPred {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ last n) :
    pred a h₁ < castPred a h₂

Proof state:
n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂

Tactic:
rw [pred_lt_castPred_iff, le_def]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem dualPairing_separatingLeft : (dualPairing 𝕜 E).SeparatingLeft

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Function.Injective ⇑(dualPairing 𝕜 E)

Tactic:
exact ContinuousLinearMap.coe_injective

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ (dualPairing 𝕜 E).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Function.Injective ⇑(dualPairing 𝕜 E)