harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem range_eq_map_coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F}
    (h : IsCompl (LinearMap.range f) G) [CompleteSpace G] (hker : ker f = ⊥) :
    LinearMap.range f =
      ((⊤ : Submodule 𝕜 E).prod (⊥ : Submodule 𝕜 G)).map
        (f.coprodSubtypeLEquivOfIsCompl h hker : E × G →ₗ[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace ↥G
hker : LinearMap.ker f = ⊥
⊢ LinearMap.range f = LinearMap.range ↑f

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace ↥G
hker : LinearMap.ker f = ⊥
⊢ LinearMap.range f = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)

Tactic:
rw [coprodSubtypeLEquivOfIsCompl, ContinuousLinearEquiv.coe_ofBijective,
  coe_coprod, LinearMap.coprod_map_prod, Submodule.map_bot, sup_bot_eq, Submodule.map_top]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (LinearMap.range f) G
inst✝ : CompleteSpace ↥G
hker : LinearMap.ker f = ⊥
⊢ LinearMap.range f = LinearMap.range ↑f
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem untrop_prod [AddCommMonoid R] (s : Finset S) (f : S → Tropical R) :
    untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map (fun i => untrop (f i)) s.val).sum

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map (fun i => untrop (f i)) s.val).sum

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)

Tactic:
convert Multiset.untrop_prod (s.val.map f)

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_iff_forall_toWeakDualBCNN_tendsto {γ : Type*} {F : Filter γ}
    {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i ↦ (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))

Tactic:
rw [tendsto_iff_weakDual_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (y : Ω →ᵇ ℝ≥0),
      Tendsto (fun i => ((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (μs i).toWeakDualBCNN) y) F
        (𝓝 (((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN) y))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (y : Ω →ᵇ ℝ≥0),
      Tendsto (fun i => ((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (μs i).toWeakDualBCNN) y) F
        (𝓝 (((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN) y))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem opNorm_neg (f : NormedAddGroupHom V₁ V₂) : ‖-f‖ = ‖f‖

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_def, coe_neg, norm_neg, Pi.neg_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
  tendsto_neg_atTop_atBot.comp this

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
have := hf.atTop_mul (neg_pos.2 hC) hg.neg

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem mem_span_support [AddZeroClass G] (f : k[G]) :
    f ∈ Submodule.span k (of k G '' (f.support : Set G))

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : k[G]
⊢ f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

Tactic:
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem calc_norm_le_one {n : ℕ} {z : ℤ_[p]} (hz : ih n z) :
    ‖(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)‖ ≤ 1 :=
  calc
    ‖(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)‖ =
        ‖(↑(F.eval z) : ℚ_[p])‖ / ‖(↑(F.derivative.eval z) : ℚ_[p])‖ :=
      norm_div _ _
    _ = ‖F.eval z‖ / ‖F.derivative.eval a‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖↑(Polynomial.eval z F)‖ / ‖↑(Polynomial.eval z (Polynomial.derivative F))‖ =
    ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
simp [hz.1]

Result:
no goals

Proof state:
case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n

Tactic:
apply hz.2

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
gcongr

Result:
case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₄_app_two :
    (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨2, by valid⟩ = app₂ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.272739, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
⊢ 2 < 4 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma cliqueSet_eq_image [NoAccidental t] : (graph t).cliqueSet 3 = toTriangle '' t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ (graph t).cliqueSet 3 ↔ x✝ ∈ ⇑toTriangle '' ↑t

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ (graph t).cliqueSet 3 ↔ x✝ ∈ ⇑toTriangle '' ↑t

Tactic:
exact is3Clique_iff

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma associator_inv_fst (X Y Z : C) :
    (α_ X Y Z).inv ≫ fst _ _ ≫ fst _ _ = fst _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.fst (product X (product Y Z).cone.pt).cone = fst X (Y ⊗ Z)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ fst (X ⊗ Y) Z ≫ fst X Y = fst X (Y ⊗ Z)

Tactic:
erw [lift_fst_assoc, lift_fst]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.fst (product X (product Y Z).cone.pt).cone = fst X (Y ⊗ Z)
-- Mathlib/ModelTheory/Substructures.lean
theorem _root_.Set.Countable.substructure_closure
    [Countable (Σl, L.Functions l)] (h : s.Countable) : Countable.{w + 1} (closure L s)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable ↑s
⊢ Countable ↥((closure L).toFun s)

Tactic:
rw [← mk_le_aleph0_iff, ← lift_le_aleph0]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable ↑s
⊢ lift.{?u.23762, w} #↥((closure L).toFun s) ≤ ℵ₀

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable ↑s
⊢ lift.{?u.23762, w} #↥((closure L).toFun s) ≤ ℵ₀

Tactic:
exact lift_card_closure_le_card_term.trans mk_le_aleph0

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
haveI : Countable s := h.to_subtype

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable ↑s
⊢ Countable ↥((closure L).toFun s)
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_distrib_subset_right {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ}
    {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε}
    (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
    image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u) :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_distrib_subset_right h_distrib

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)

Tactic:
exact Set.image2_distrib_subset_right h_distrib

Result:
no goals

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ ↑(image₂ f (image₂ g s t) u) ⊆ ↑(image₂ g' (image₂ f₁ s u) (image₂ f₂ t u))

Tactic:
push_cast

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem ae_eq_of_ae_subset_of_measure_ge (h₁ : s ≤ᵐ[μ] t) (h₂ : μ t ≤ μ s)
    (hsm : NullMeasurableSet s μ) (ht : μ t ≠ ∞) : s =ᵐ[μ] t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
h₂ : μ t ≤ μ s
hsm : NullMeasurableSet s μ
ht : μ t ≠ ⊤
⊢ s =ᶠ[ae μ] t

Tactic:
refine eventuallyLE_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
h₂ : μ t ≤ μ s
hsm : NullMeasurableSet s μ
ht : μ t ≠ ⊤
⊢ μ (t \ s) = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
ht : μ t ≠ ⊤
h₂ : μ t = μ s
⊢ μ (t \ s) = 0

Tactic:
replace ht : μ s ≠ ∞ := h₂ ▸ ht

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ⊤
⊢ μ (t \ s) = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ⊤
⊢ μ (t \ s) = 0

Tactic:
rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
h₂ : μ t ≤ μ s
hsm : NullMeasurableSet s μ
ht : μ t ≠ ⊤
⊢ μ (t \ s) = 0

Tactic:
replace h₂ : μ t = μ s := h₂.antisymm (measure_mono_ae h₁)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
ht : μ t ≠ ⊤
h₂ : μ t = μ s
⊢ μ (t \ s) = 0
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem opProductIsoCoproduct'_inv_comp_lift {f : Fan Z} {c : Cofan (op <| Z ·)}
    (hf : IsLimit f) (hc : IsColimit c) (f' : Fan Z) :
    (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ ((hf.lift f').op.unop ≫ f.π.app { as := j }).op =
    (((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op).unop ≫ f.π.app { as := j }).op

Tactic:
simp only [Discrete.functor_obj, unop_op, Quiver.Hom.unop_op, IsLimit.fac, Fan.op, unop_comp,
  Category.assoc, op_comp, op_unop, Quiver.Hom.op_unop]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op =
    (f.π.app { as := j }).op ≫
      (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun a => (f'.proj a).op)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op =
    (f.π.app { as := j }).op ≫
      (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun a => (f'.proj a).op)

Tactic:
erw [← Category.assoc, proj_comp_opProductIsoCoproduct'_hom, IsColimit.fac]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op = (Cofan.mk (op f'.pt) fun a => (f'.proj a).op).ι.app { as := j }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op = (Cofan.mk (op f'.pt) fun a => (f'.proj a).op).ι.app { as := j }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
⊢ (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op

Tactic:
refine (Iso.inv_comp_eq _).mpr (Quiver.Hom.unop_inj (hf.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x => op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ ((hf.lift f').op.unop ≫ f.π.app { as := j }).op =
    (((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op).unop ≫ f.π.app { as := j }).op
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsConj.isReal_comp (h : IsConj φ σ) : IsReal (φ.comp (algebraMap k K))

Proof state:
case a
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
h : IsConj φ σ
x : k
⊢ (star (φ.comp (algebraMap k K))) x = (φ.comp (algebraMap k K)) x

Tactic:
simp only [conjugate_coe_eq, RingHom.coe_comp, Function.comp_apply, ← h.eq,
  starRingEnd_apply, AlgEquiv.commutes]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
h : IsConj φ σ
⊢ IsReal (φ.comp (algebraMap k K))

Tactic:
ext1 x

Result:
case a
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
h : IsConj φ σ
x : k
⊢ (star (φ.comp (algebraMap k K))) x = (φ.comp (algebraMap k K)) x
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[reassoc]
lemma prop.fac {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) :
    f = Φ.toSucc X ≫ eqToHom hf.succ_eq

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ f = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
cases hf

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X : C
⊢ Φ.toSucc X = Φ.toSucc X ≫ eqToHom ⋯

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X : C
⊢ Φ.toSucc X = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
    l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray

Proof state:
α : Type u_1
l : List α
i j : Nat
hi : i < l.toArray.size
hj : j < l.toArray.size
⊢ l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
i j : Nat
hi : i < l.toArray.size
hj : j < l.toArray.size
⊢ (l.toArray.swap i j hi hj).toList = ((l.set i l[j]).set j l[i]).toArray.toList

Proof state:
case h
α : Type u_1
l : List α
i j : Nat
hi : i < l.toArray.size
hj : j < l.toArray.size
⊢ (l.toArray.swap i j hi hj).toList = ((l.set i l[j]).set j l[i]).toArray.toList

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem Splits.comp_X_add_C (a : K) {f : K[X]}
    (h : f.Splits i) : (f.comp (X + C a)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (-a)) h

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
a : K
f : K[X]
h : Splits i f
⊢ (X + C a).degree ≤ 1

Tactic:
simpa using degree_X_sub_C_le (-a)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_piCongrLeft (f : ι' ≃ ι) :
    MeasurePreserving (MeasurableEquiv.piCongrLeft α f)
      (Measure.pi fun i' => μ (f i')) (Measure.pi μ) where
  measurable := (MeasurableEquiv.piCongrLeft α f).measurable
  map_eq

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
⊢ Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' => μ (f i')) = Measure.pi μ

Tactic:
refine (pi_eq fun s _ => ?_).symm

Result:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' => μ (f i'))) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' => μ (f i'))) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
  Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  (atTop_basis.tendsto_iff nhds_basis_ball).trans <| by
    simp only [true_and, mem_ball, mem_Ici]

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε

Tactic:
simp only [true_and, mem_ball, mem_Ici]

Result:
no goals