harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Num/Lemmas.lean
theorem div_to_int : ∀ n d, ((n / d : ZNum) : ℤ) = n / d
  | 0, 0 => by simp [Int.ediv_zero]
  | 0, pos _ => (Int.zero_ediv _).symm
  | 0, neg _ => (Int.zero_ediv _).symm
  | pos _, 0 => (Int.ediv_zero _).symm
  | neg _, 0 => (Int.ediv_zero _).symm
  | pos n, pos d => (Num.cast_toZNum _).trans <| by rw [← Num.to_nat_to_int]; simp
  | pos n, neg d => (Num.cast_toZNumNeg _).trans <| by rw [← Num.to_nat_to_int]; simp
  | neg n, pos d =>
    show -_ = -_ / ↑d by
      rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]
      change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]
      rw [d.to_nat_eq_succ_pred]
  | neg n, neg d =>
    show ↑(PosNum.pred' n / Num.pos d).succ' = -_ / -↑d by
      rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]
      change (Nat.succ (_ / d) : ℤ) = Nat.succ (n.pred' / (d.pred' + 1))
      rw [d.to_nat_eq_succ_pred]

Proof state:
n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -↑n / -↑d

Tactic:
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
  Num.div_to_nat]

Result:
n d : PosNum
⊢ ↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)

Proof state:
n d : PosNum
⊢ -[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]

Tactic:
rw [d.to_nat_eq_succ_pred]

Result:
no goals

Proof state:
n d : PosNum
⊢ ↑↑(n.div' d) = ↑(pos n) / ↑(pos d)

Tactic:
simp

Result:
no goals

Proof state:
n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -↑n / ↑d

Tactic:
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
  Num.div_to_nat]

Result:
n d : PosNum
⊢ -↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)

Proof state:
n d : PosNum
⊢ ↑(↑n.pred' / ↑d).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ

Tactic:
rw [d.to_nat_eq_succ_pred]

Result:
no goals

Proof state:
n d : PosNum
⊢ -↑(n.div' d) = ↑(pos n) / ↑(neg d)

Tactic:
rw [← Num.to_nat_to_int]

Result:
n d : PosNum
⊢ -↑↑(n.div' d) = ↑(pos n) / ↑(neg d)

Proof state:
n d : PosNum
⊢ ↑(n.div' d) = ↑(pos n) / ↑(pos d)

Tactic:
rw [← Num.to_nat_to_int]

Result:
n d : PosNum
⊢ ↑↑(n.div' d) = ↑(pos n) / ↑(pos d)

Proof state:
n d : PosNum
⊢ -↑↑(n.div' d) = ↑(pos n) / ↑(neg d)

Tactic:
simp

Result:
no goals

Proof state:
⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
simp [Int.ediv_zero]

Result:
no goals

Proof state:
n d : PosNum
⊢ ↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)

Tactic:
change (Nat.succ (_ / d) : ℤ) = Nat.succ (n.pred' / (d.pred' + 1))

Result:
n d : PosNum
⊢ ↑(↑n.pred' / ↑d).succ = ↑(↑n.pred' / (↑d.pred' + 1)).succ

Proof state:
n d : PosNum
⊢ -↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)

Tactic:
change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]

Result:
n d : PosNum
⊢ -[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_subset_biUnion_of_subset_left (t : α → Finset β) (h : s₁ ⊆ s₂) :
    s₁.biUnion t ⊆ s₂.biUnion t := fun x ↦ by
  simp only [and_imp, mem_biUnion, exists_prop]; exact Exists.imp fun a ha ↦ ⟨h ha.1, ha.2⟩

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ (∃ a ∈ s₁, x ∈ t a) → ∃ a ∈ s₂, x ∈ t a

Tactic:
exact Exists.imp fun a ha ↦ ⟨h ha.1, ha.2⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ x ∈ s₁.biUnion t → x ∈ s₂.biUnion t

Tactic:
simp only [and_imp, mem_biUnion, exists_prop]

Result:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ (∃ a ∈ s₁, x ∈ t a) → ∃ a ∈ s₂, x ∈ t a
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem join_map_join (μ : Measure (Measure (Measure α))) : join (map join μ) = join (join μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ (map join μ).join = μ.join.join

Tactic:
show bind μ join = join (join μ)

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.join.join

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.bind fun a => (id a).bind id

Tactic:
apply congr_arg (bind μ)

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ join = fun a => (id a).bind id

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ join = fun a => (id a).bind id

Tactic:
funext ν

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ ν.join = (id ν).bind id

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.join.join

Tactic:
rw [join_eq_bind, join_eq_bind, bind_bind measurable_id measurable_id]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.bind fun a => (id a).bind id

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ ν.join = (id ν).bind id

Tactic:
exact join_eq_bind ν

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem alternatingProd_reverse :
    ∀ l : List α, alternatingProd (reverse l) = alternatingProd l ^ (-1 : ℤ) ^ (length l + 1)
  | [] => by simp only [alternatingProd_nil, one_zpow, reverse_nil]
  | a :: l => by
    simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]
    rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
l : List α
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
  alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
  Int.neg_mul, one_mul, zpow_neg, inv_inv]

Result:
α : Type u_2
inst✝ : CommGroup α
a : α
l : List α
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
l : List α
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length

Tactic:
rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommGroup α
⊢ [].reverse.alternatingProd = [].alternatingProd ^ (-1) ^ ([].length + 1)

Tactic:
simp only [alternatingProd_nil, one_zpow, reverse_nil]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_comp_of_eq {x : M} {y : M'} (hg : MDifferentiableAt I' I'' g y)
    (hf : MDifferentiableAt I I' f x) (hy : f x = y) :
    mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
x : M
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableAt I I' f x
hy : f x = y
⊢ mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
x : M
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
x : M
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Tactic:
exact mfderiv_comp x hg hf

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
/-- If `f` is a linear map from `M₁` to `M₂` that preserves the quadratic forms, and if it has
a linear retraction `g` that also preserves the quadratic forms, then `CliffordAlgebra.map g`
is a retraction of `CliffordAlgebra.map f`. -/
lemma leftInverse_map_of_leftInverse {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
    (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁) (h : LeftInverse g f) : LeftInverse (map g) (map f)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
⊢ LeftInverse ⇑(map g) ⇑(map f)

Tactic:
refine fun x => ?_

Result:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
x : CliffordAlgebra Q₁
⊢ (map g) ((map f) x) = x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
x : CliffordAlgebra Q₁
⊢ (map g) ((map f) x) = x

Tactic:
replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h

Result:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map g) ((map f) x) = x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map g) ((map f) x) = x

Tactic:
rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem tail_map {β : Type*} (v : Vector α (n + 1)) (f : α → β) :
    (v.map f).tail = v.tail.map f

Proof state:
case intro.intro
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).tail = map f v.tail

Tactic:
rw [h, map_cons, tail_cons, tail_cons]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).tail = map f v.tail

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Result:
case intro.intro
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).tail = map f v.tail
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem le_comap_primeCompl_iff {J : Ideal P} [J.IsPrime] {f : R →+* P} :
    I.primeCompl ≤ J.primeCompl.comap f ↔ J.comap f ≤ I :=
  ⟨fun h x hx => by
    contrapose! hx
    exact h hx,
   fun h _ hx hfxJ => hx (h hfxJ)⟩

Proof state:
R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∉ I
⊢ x ∉ Ideal.comap f J

Tactic:
exact h hx

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∈ Ideal.comap f J
⊢ x ∈ I

Tactic:
contrapose! hx

Result:
R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∉ I
⊢ x ∉ Ideal.comap f J
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_inv_apply_right : SameCycle f x (f⁻¹ y) ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x (f⁻¹ y) ↔ f.SameCycle x y

Tactic:
rw [← sameCycle_apply_right, apply_inv_self]

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndepSet_iff_condIndep (s t : Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepSet m' hm' s t μ ↔ CondIndep m' (generateFrom {s}) (generateFrom {t}) hm' μ

Proof state:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔ CondIndep m' (generateFrom {s}) (generateFrom {t}) hm' μ

Tactic:
simp only [CondIndepSet, CondIndep, Kernel.IndepSet]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type*)
    [m : MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] :
    ∃ _ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Proof state:
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩

Result:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Proof state:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
let F := f.toEquiv.toHomeomorphOfIsInducing <| .induced _

Result:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
F : α ≃ₜ ↑s := f.toHomeomorphOfIsInducing ⋯
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Proof state:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
F : α ≃ₜ ↑s := f.toHomeomorphOfIsInducing ⋯
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
exact ⟨inferInstance, F.secondCountableTopology, F.symm.t4Space,
  f.measurableEmbedding.borelSpace F.isInducing⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
letI := induced f inferInstance

Result:
case intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
-- Mathlib/Data/Matrix/Reflection.lean
theorem forall_iff : ∀ {m n} (P : Matrix (Fin m) (Fin n) α → Prop), Forall P ↔ ∀ x, P x
  | 0, _, _ => Iff.symm Fin.forall_fin_zero_pi
  | m + 1, n, P => by
    simp only [Forall, FinVec.forall_iff, forall_iff]
    exact Iff.symm Fin.forall_fin_succ_pi

Proof state:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
simp only [Forall, FinVec.forall_iff, forall_iff]

Result:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α), P (of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Proof state:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α), P (of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
exact Iff.symm Fin.forall_fin_succ_pi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
    (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Array α
⊢ (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : K[X]) (hq : degree q = 1) :
    eigenspace f (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (aeval f q) :=
  calc
    eigenspace f (-q.coeff 0 / q.leadingCoeff)
    _ = LinearMap.ker (q.leadingCoeff • f - algebraMap K (End K V) (-q.coeff 0))

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0))) = LinearMap.ker ((aeval f) q)

Tactic:
rwa [← eq_X_add_C_of_degree_eq_one]

Result:
no goals

Proof state:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : ⊥ = 1
h : q.leadingCoeff = 0
⊢ False

Tactic:
cases hq

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ f.eigenspace (-q.coeff 0 / q.leadingCoeff) =
    LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0))

Tactic:
rw [eigenspace_div]

Result:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.leadingCoeff ≠ 0

Proof state:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.leadingCoeff ≠ 0

Tactic:
intro h

Result:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
h : q.leadingCoeff = 0
⊢ False

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))

Tactic:
simp [algebraMap, Algebra.algebraMap]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0)))

Tactic:
rw [C_mul', aeval_def]

Result:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))

Proof state:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
h : q.leadingCoeff = 0
⊢ False

Tactic:
rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq

Result:
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : ⊥ = 1
h : q.leadingCoeff = 0
⊢ False
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem setCurr : ∀ {it}, Valid it → Valid (it.setCurr c)
  | it, h => by
    let ⟨l, r, h⟩ := h.validFor
    exact h.setCurr'.valid

Proof state:
c : Char
it : Iterator
h : it.Valid
⊢ (it.setCurr c).Valid

Tactic:
let ⟨l, r, h⟩ := h.validFor

Result:
c : Char
it : Iterator
h✝ : it.Valid
l r : List Char
h : ValidFor l r it
⊢ (it.setCurr c).Valid

Proof state:
c : Char
it : Iterator
h✝ : it.Valid
l r : List Char
h : ValidFor l r it
⊢ (it.setCurr c).Valid

Tactic:
exact h.setCurr'.valid

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem coe_injective : @Function.Injective (NormedAddGroupHom V₁ V₂) (V₁ → V₂) toFun

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
⊢ Function.Injective toFun

Tactic:
apply coe_inj

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_eq_end_iff {m : ι} : hitting u s n m ω = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
⊢ hitting u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m

Tactic:
classical
rw [hitting, ite_eq_right_iff]

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
⊢ hitting u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m

Tactic:
rw [hitting, ite_eq_right_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_right_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
    ⟪v i, linearCombination 𝕜 v l⟫ = l i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ inner (v i) ((linearCombination 𝕜 v) l) = l i

Tactic:
simpa [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv] using Eq.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ inner (v i) ((linearCombination 𝕜 v) l) = l i

Tactic:
classical
simpa [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv] using Eq.symm

Result:
no goals