harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem Subsingleton.stronglyMeasurable [Subsingleton β] (f : α → β) : StronglyMeasurable f

Proof state:
case h
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
y : α
⊢ y ∈ f ⁻¹' {x} ↔ y ∈ univ

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
have h_univ : f ⁻¹' {x} = Set.univ := by
  ext1 y
  simp [eq_iff_true_of_subsingleton]

Result:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet (f ⁻¹' {x})

Proof state:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
rw [h_univ]

Result:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet univ

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
⊢ StronglyMeasurable f

Tactic:
let f_sf : α →ₛ β := ⟨f, fun x => ?_, Set.Subsingleton.finite Set.subsingleton_of_subsingleton⟩

Result:
case refine_2
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ MeasurableSet (f ⁻¹' {x})

Proof state:
case refine_2
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨fun _ => f_sf, fun x => tendsto_const_nhds⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ f ⁻¹' {x} = univ

Tactic:
ext1 y

Result:
case h
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
y : α
⊢ y ∈ f ⁻¹' {x} ↔ y ∈ univ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet univ

Tactic:
exact MeasurableSet.univ

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem secondCountable_of_almost_dense_set
    (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ) :
    SecondCountableTopology α

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
t : Set α
htc : t.Countable
ht : univ ⊆ closure t
⊢ SeparableSpace α

Tactic:
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
⊢ ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε

Tactic:
simpa only [univ_subset_iff] using hs

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
⊢ SeparableSpace α

Tactic:
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
t : Set α
htc : t.Countable
ht : univ ⊆ closure t
⊢ SeparableSpace α

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
⊢ SeparableSpace α

Tactic:
have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε := by
  simpa only [univ_subset_iff] using hs

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
⊢ SeparableSpace α

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ
⊢ SeparableSpace α
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem inertiaDeg_algebraMap [P.LiesOver p] [p.IsMaximal] :
    inertiaDeg p P = finrank (R ⧸ p) (S ⧸ P)

Proof state:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : P.LiesOver p
inst✝ : p.IsMaximal
a✝ : Nontrivial (S ⧸ P)
⊢ p.inertiaDeg P = finrank (R ⧸ p) (S ⧸ P)

Tactic:
rw [inertiaDeg, dif_pos (over_def P p).symm]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : P.LiesOver p
inst✝ : p.IsMaximal
⊢ p.inertiaDeg P = finrank (R ⧸ p) (S ⧸ P)

Tactic:
nontriviality S ⧸ P using inertiaDeg_of_subsingleton, finrank_zero_of_subsingleton

Result:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : P.LiesOver p
inst✝ : p.IsMaximal
a✝ : Nontrivial (S ⧸ P)
⊢ p.inertiaDeg P = finrank (R ⧸ p) (S ⧸ P)
-- Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
@[simp]
lemma OneTruncation₂.homOfEq_edge
    {X : SSet.Truncated.{u} 2} {x₁ y₁ x₂ y₂ : OneTruncation₂ X}
    (f : x₁ ⟶ y₁) (hx : x₁ = x₂) (hy : y₁ = y₂) :
    (Quiver.homOfEq f hx hy).edge = f.edge

Proof state:
X : Truncated 2
x₁ y₁ : OneTruncation₂ X
f : x₁ ⟶ y₁
⊢ (Quiver.homOfEq f ⋯ ⋯).edge = f.edge

Tactic:
rfl

Result:
no goals

Proof state:
X : Truncated 2
x₁ y₁ x₂ y₂ : OneTruncation₂ X
f : x₁ ⟶ y₁
hx : x₁ = x₂
hy : y₁ = y₂
⊢ (Quiver.homOfEq f hx hy).edge = f.edge

Tactic:
subst hx hy

Result:
X : Truncated 2
x₁ y₁ : OneTruncation₂ X
f : x₁ ⟶ y₁
⊢ (Quiver.homOfEq f ⋯ ⋯).edge = f.edge
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is one if the characteristic is zero. -/
lemma expChar_one_of_char_zero (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] : q = 1

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1

Tactic:
rcases hq with q | hq_prime

Result:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1

Proof state:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1

Tactic:
exact False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

Result:
no goals
-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem solution_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
    solution p a₁ a₂ ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ False

Tactic:
have := solution_spec p a₁ a₂

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hp.out.one_lt

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ solution p a₁ a₂ ≠ 0

Tactic:
intro h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
rw [h, zero_pow] at this

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem map_id : map (LinearMap.id : M →ₗ[R'] M) = AlgHom.id R' _

Proof state:
case h
R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ ∀ (m : M), (map LinearMap.id) (inr m) = (AlgHom.id R' (tsze R' M)) (inr m)

Tactic:
simp only [map_inr, LinearMap.id_coe, id_eq, AlgHom.coe_id, forall_const]

Result:
no goals

Proof state:
R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ map LinearMap.id = AlgHom.id R' (tsze R' M)

Tactic:
apply algHom_ext

Result:
case h
R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ ∀ (m : M), (map LinearMap.id) (inr m) = (AlgHom.id R' (tsze R' M)) (inr m)
-- Mathlib/Topology/Filter.lean
theorem nhds_bot : 𝓝 (⊥ : Filter α) = pure ⊥

Proof state:
α : Type u_2
⊢ 𝓝 ⊥ = pure ⊥

Tactic:
simp [nhds_eq, Function.comp_def, lift'_bot monotone_principal.Iic]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem ker_comp_eq_of_commute_of_disjoint_ker [FiniteDimensional K V] {f g : V →ₗ[K] V}
    (h : Commute f g) (h' : Disjoint (ker f) (ker g)) :
    ker (f ∘ₗ g) = ker f ⊔ ker g

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ∀ x ∈ ker f, g x ∈ ker f

Tactic:
simpa

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ker (f ∘ₗ g) = ker f ⊔ ker g

Tactic:
rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ∀ x ∈ ker f, g x ∈ ker f

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
⊢ ker (f ∘ₗ g) = ker f ⊔ ker g

Tactic:
suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
⊢ ∀ (x : V), f x = 0 → f (g x) = 0

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
x : V
hx : f x = 0
⊢ f (g x) = 0

Tactic:
rw [← comp_apply, ← mul_eq_comp, h.eq, mul_apply, hx, _root_.map_zero]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
⊢ ∀ (x : V), f x = 0 → f (g x) = 0

Tactic:
intro x hx

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint (ker f) (ker g)
x : V
hx : f x = 0
⊢ f (g x) = 0
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_of_degree_sub_lt_of_eval_index_eq (hvs : Set.InjOn v s)
    (degree_fg_lt : (f - g).degree < #s) (eval_fg : ∀ i ∈ s, f.eval (v i) = g.eval (v i)) :
    f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) (f - g) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f = eval (v i) g

Tactic:
exact eval_fg

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) (f - g) = 0

Tactic:
simp_rw [eval_sub, sub_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f = eval (v i) g
-- Mathlib/Algebra/Quaternion.lean
theorem mul_imK : (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re :=
  (QuaternionAlgebra.mul_imK a b).trans <| by ring

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ + 0 * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re

Tactic:
ring

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem exists_subseq_of_forall_mem_union {s t : Set α} (e : ℕ → α) (he : ∀ n, e n ∈ s ∪ t) :
    ∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ ∀ n, e (g n) ∈ t

Proof state:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)

Tactic:
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
  Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

case inr
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
classical
  have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
    simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
      Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
  cases this
  exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
    ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
cases this

Result:
case inl
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

case inr
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Proof state:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]

Result:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t
-- Mathlib/Topology/Filter.lean
theorem mem_interior {s : Set (Filter α)} {l : Filter α} :
    l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Proof state:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem sub_int_iff : LiouvilleWith p (x - m) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_intCast, sub_rat_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_sub (m n : ℕ) : ((m - n : ℕ) : Ordinal) = m - n

Proof state:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [← add_left_cancel_iff (a := ↑n), ← Nat.cast_add, add_tsub_cancel_of_le h,
  Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)]

Result:
no goals

Proof state:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_total m n with h | h

Result:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₂Γ₂_inv_app_f_f (X : Karoubi (ChainComplex C ℕ)) (n : ℕ) :
    (N₂Γ₂.inv.app X).f.f n =
      X.p.f n ≫ ((Γ₀.splitting X.X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌))

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ ((𝟭 (Karoubi (ChainComplex C ℕ))).map X.decompId_i).f.f n ≫
      X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) =
    X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
apply Karoubi.HomologicalComplex.p_idem_assoc

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ (N₂Γ₂.inv.app X).f.f n = X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
dsimp [N₂Γ₂]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ ((((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
                    (toKaroubi (ChainComplex C ℕ))).preimage
                (N₁Γ₀.inv ≫ N₂Γ₂ToKaroubiIso.inv)).app
            X).f.f
      n =
    X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ ((((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
                    (toKaroubi (ChainComplex C ℕ))).preimage
                (N₁Γ₀.inv ≫ N₂Γ₂ToKaroubiIso.inv)).app
            X).f.f
      n =
    X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
  Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,
  N₁Γ₀_inv_app_f_f, toKaroubi_obj_X, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
  Γ₀.obj_obj, PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f,
  Γ₂_map_f_app, unop_op, Karoubi.decompId_p_f, PInfty_f_idem_assoc,
  PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk,
  Splitting.ι_desc]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ ((𝟭 (Karoubi (ChainComplex C ℕ))).map X.decompId_i).f.f n ≫
      X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) =
    X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem funMulInvSnorm_rpow {p : ℝ} (hp0 : 0 < p) {f : α → ℝ≥0∞} {a : α} :
    funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ c, f c ^ p ∂μ)⁻¹

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
suffices h_inv_rpow : ((∫⁻ c : α, f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ c : α, f c ^ p ∂μ)⁻¹ by
  rw [h_inv_rpow]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
h_inv_rpow : ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [h_inv_rpow]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
rw [funMulInvSnorm, mul_rpow_of_nonneg _ _ (le_of_lt hp0)]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹