harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem hasStrictInitialObjects_of_initial_is_strict [HasInitial C]
    (h : ∀ (A) (f : A ⟶ ⊥_ C), IsIso f) : HasStrictInitialObjects C :=
  { out := fun {I A} f hI =>
      haveI := h A (f ≫ hI.to _)
      ⟨⟨hI.to _ ≫ inv (f ≫ hI.to (⊥_ C)), by rw [← assoc, IsIso.hom_inv_id], hI.hom_ext _ _⟩⟩ }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ hI.to (⊥_ C))
⊢ f ≫ hI.to (⊥_ C) ≫ inv (f ≫ hI.to (⊥_ C)) = 𝟙 A

Tactic:
rw [← assoc, IsIso.hom_inv_id]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem not_disjoint_iff : ¬Disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t :=
  disjoint_left.not.trans <| not_forall.trans <| exists_congr fun _ => by
    rw [Classical.not_imp, not_not]

Proof state:
α : Type u_1
s t : Finset α
x✝ : α
⊢ ¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
rw [Classical.not_imp, not_not]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean
theorem isRightAdjoint_TFAE (u : b ⟶ a) :
    List.TFAE [
      IsRightAdjoint u,
      HasAbsLeftKanLift u (𝟙 a),
      ∃ _ : HasLeftKanLift u (𝟙 a), LanLift.CommuteWith u (𝟙 a) u]

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 2 → 3
| h => ⟨inferInstance, inferInstance⟩

Result:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 1 → 2
| h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift

Result:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
tfae_3_to_1 : (∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u) → IsRightAdjoint u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 3 → 1
| ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u

Result:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
tfae_3_to_1 : (∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u) → IsRightAdjoint u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE
-- Mathlib/RingTheory/Artinian/Ring.lean
theorem isUnit_submonoid_eq : IsUnit.submonoid R = R⁰

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰

Tactic:
simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsUnit.submonoid R = R⁰

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma pushoutCocone_inl_eq_inr_iff_of_iso {c c' : PushoutCocone f g} (e : c ≅ c')
    (x₁ : X₁) (x₂ : X₂) :
    c.inl x₁ = c.inr x₂ ↔ c'.inl x₁ = c'.inr x₂

Proof state:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ c'.inl x₁ = c'.inr x₂ → c.inl x₁ = c.inr x₂

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ c.inl x₁ = c.inr x₂ ↔ c'.inl x₁ = c'.inr x₂

Tactic:
constructor

Result:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ c.inl x₁ = c.inr x₂ → c'.inl x₁ = c'.inr x₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ c'.inl x₁ = c'.inr x₂ → c.inl x₁ = c.inr x₂

Proof state:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ c.inl x₁ = c.inr x₂ → c'.inl x₁ = c'.inr x₂

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem mem_chartAt_source_of_eq_one {i : ι} {x : M} (h : fs i x = 1) :
    x ∈ (chartAt H (fs.c i)).source :=
  (fs i).support_subset_source <| by simp [h]

Proof state:
ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(fs.toFun i) x = 1
⊢ x ∈ support ↑(fs.toFun i)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_norm_le : ‖orthogonalProjection K‖ ≤ 1 :=
  LinearMap.mkContinuous_norm_le _ (by norm_num) _

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ 0 ≤ 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₁₂_iff : (graph t).Adj (in₁ b) (in₂ c) ↔ ∃ a, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₁₂ h⟩

Proof state:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (graph t).Adj (in₁ b) (in₂ c) → ∃ a, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setLIntegral_rnDeriv_mul [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {f : α → ℝ≥0∞}
    (hf : AEMeasurable f ν) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ x in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [setLIntegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf hs]

Result:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
nth_rw 2 [← Measure.withDensity_rnDeriv_eq μ ν hμν]

Result:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν

Tactic:
simp only [Pi.mul_apply]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkSpecializes_refl {C : Type*} [Category C] [Limits.HasColimits C] {X : TopCat}
    (F : X.Presheaf C) (x : X) : F.stalkSpecializes (specializes_refl x) = 𝟙 _

Proof state:
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
⊢ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)

Tactic:
ext

Result:
case ih
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : x ∈ U✝
⊢ F.germ U✝ x hxU✝ ≫ F.stalkSpecializes ⋯ = F.germ U✝ x hxU✝ ≫ 𝟙 (F.stalk x)

Proof state:
case ih
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : x ∈ U✝
⊢ F.germ U✝ x hxU✝ ≫ F.stalkSpecializes ⋯ = F.germ U✝ x hxU✝ ≫ 𝟙 (F.stalk x)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_comm (a b : Nimber) : a * b = b * a

Proof state:
a b : Nimber
⊢ a * b = b * a

Tactic:
apply le_antisymm <;> refine mul_le_of_forall_ne fun x hx y hy ↦ ?_

Result:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ x * b + a * y + x * y ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ x * a + b * y + x * y ≠ a * b

Proof state:
case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ y * b + a * x + y * x ≠ a * b

Tactic:
exact mul_ne_of_lt y hy x hx

Result:
no goals

Proof state:
case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ x * a + b * y + x * y ≠ a * b

Tactic:
rw [add_comm (x * _), ← Nimber.mul_comm y, ← Nimber.mul_comm a, ← Nimber.mul_comm y]

Result:
case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ y * b + a * x + y * x ≠ a * b

Proof state:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ y * a + b * x + y * x ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ y * b + a * x + y * x ≠ a * b

Tactic:
all_goals exact mul_ne_of_lt y hy x hx

Result:
no goals

Proof state:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ x * b + a * y + x * y ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ x * a + b * y + x * y ≠ a * b

Tactic:
on_goal 1 => rw [add_comm (x * _), Nimber.mul_comm a, Nimber.mul_comm x, Nimber.mul_comm x]

Result:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ y * a + b * x + y * x ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ x * a + b * y + x * y ≠ a * b

Proof state:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ x * b + a * y + x * y ≠ b * a

Tactic:
rw [add_comm (x * _), Nimber.mul_comm a, Nimber.mul_comm x, Nimber.mul_comm x]

Result:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ y * a + b * x + y * x ≠ b * a

Proof state:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ y * a + b * x + y * x ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ x * a + b * y + x * y ≠ a * b

Tactic:
on_goal 2 => rw [add_comm (x * _), ← Nimber.mul_comm y, ← Nimber.mul_comm a, ← Nimber.mul_comm y]

Result:
case a
a b x : Nimber
hx : x < a
y : Nimber
hy : y < b
⊢ y * a + b * x + y * x ≠ b * a

case a
a b x : Nimber
hx : x < b
y : Nimber
hy : y < a
⊢ y * b + a * x + y * x ≠ a * b
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_primeIdealOf (x : U) :
    hU.fromSpec.base (hU.primeIdealOf x) = x.1

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom U.ι.base) x = ↑x

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom hU.fromSpec.base) (hU.primeIdealOf x) = ↑x

Tactic:
dsimp only [IsAffineOpen.fromSpec, Subtype.coe_mk, IsAffineOpen.primeIdealOf]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (hU.isoSpec.inv ≫ U.ι).base) ((ConcreteCategory.hom hU.isoSpec.hom.base) x) = ↑x

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (hU.isoSpec.inv ≫ U.ι).base) ((ConcreteCategory.hom hU.isoSpec.hom.base) x) = ↑x

Tactic:
rw [← Scheme.comp_base_apply, Iso.hom_inv_id_assoc]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom U.ι.base) x = ↑x
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive] lemma le_prod_of_mem (ha : a ∈ m) : a ≤ m.prod

Proof state:
case intro
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a : α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod

Tactic:
exact _root_.le_mul_right (le_refl a)

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a : α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod

Tactic:
rw [prod_cons]

Result:
case intro
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a : α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod

Proof state:
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
m : Multiset α
a : α
ha : a ∈ m
⊢ a ≤ m.prod

Tactic:
obtain ⟨t, rfl⟩ := exists_cons_of_mem ha

Result:
case intro
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a : α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem mult_pos {w : InfinitePlace K} : 0 < mult w

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 0 < if w.IsReal then 1 else 2

Tactic:
split_ifs <;> norm_num

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 0 < w.mult

Tactic:
rw [mult]

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ 0 < if w.IsReal then 1 else 2
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive] lemma prod_eq_one_iff : l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
  ⟨all_one_of_le_one_le_of_prod_eq_one fun _ _ => one_le _, fun h => by
    rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
    · exact (length l)
    · rfl⟩

Proof state:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

Tactic:
exact (length l)

Result:
no goals

Proof state:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]

Result:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?m.19380

Proof state:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = l.length

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_insert_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ : P} (h₁ : p₁ ∈ line[k, p₃, p₄])
    (h₂ : p₂ ∈ line[k, p₃, p₄]) : Collinear k ({p₁, p₂, p₃, p₄} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : p₁ ∈ affineSpan k {p₃, p₄}
h₂ : p₂ ∈ affineSpan k {p₃, p₄}
⊢ Collinear k {p₁, p₂, p₃, p₄}

Tactic:
rw [collinear_insert_iff_of_mem_affineSpan
    ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₁),
  collinear_insert_iff_of_mem_affineSpan h₂]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : p₁ ∈ affineSpan k {p₃, p₄}
h₂ : p₂ ∈ affineSpan k {p₃, p₄}
⊢ Collinear k {p₃, p₄}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
h₁ : p₁ ∈ affineSpan k {p₃, p₄}
h₂ : p₂ ∈ affineSpan k {p₃, p₄}
⊢ Collinear k {p₃, p₄}

Tactic:
exact collinear_pair _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem isPiSystem_Ioi_rat : IsPiSystem (⋃ a : ℚ, {Ioi (a : ℝ)})

Proof state:
⊢ IsPiSystem (⋃ a, {Ioi ↑a})

Tactic:
convert isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)

Result:
case h.e'_2

⊢ ⋃ a, {Ioi ↑a} = Ioi '' (Rat.cast '' univ)

Proof state:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Ioi ↑a} ↔ x ∈ Ioi '' (Rat.cast '' univ)

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Result:
no goals

Proof state:
case h.e'_2

⊢ ⋃ a, {Ioi ↑a} = Ioi '' (Rat.cast '' univ)

Tactic:
ext x

Result:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Ioi ↑a} ↔ x ∈ Ioi '' (Rat.cast '' univ)
-- Mathlib/Analysis/Complex/Basic.lean
@[simp]
lemma ofReal_mem_slitPlane {x : ℝ} : ↑x ∈ slitPlane ↔ 0 < x

Proof state:
x : ℝ
⊢ ↑x ∈ slitPlane ↔ 0 < x

Tactic:
simp [mem_slitPlane_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNFRec_pos (b : Ordinal) {o : Ordinal} {C : Ordinal → Sort*} (ho : o ≠ 0) (H0 : C 0)
    (H : ∀ o, o ≠ 0 → C (o % b ^ log b o) → C o) :
    CNFRec b H0 H o = H o ho (@CNFRec b C H0 H _)

Proof state:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ b.CNFRec H0 H o = H o ho (b.CNFRec H0 H (o % b ^ log b o))

Tactic:
rw [CNFRec, dif_neg]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
private lemma antilipschitzWith_toMatrixAux :
    AntilipschitzWith (Fintype.card m * Fintype.card n)
      (ofMatrixₗ.symm (R := ℂ) : CStarMatrix m n A → Matrix m n A)

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝ : i ∈ Finset.univ
⊢ ∑ i_1 : n, ‖M i i_1 * v i_1‖ ≤ ∑ i_1 : n, ‖M i i_1‖ * ‖v‖

Tactic:
gcongr with j _

Result:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j * v j‖ ≤ ‖M i j‖ * ‖v‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ AntilipschitzWith (↑(Fintype.card m) * ↑(Fintype.card n)) ⇑ofMatrixₗ.symm

Tactic:
refine AddMonoidHomClass.antilipschitz_of_bound _ fun M => ?_

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖M‖ ≤ ↑(↑(Fintype.card m) * ↑(Fintype.card n)) * ‖ofMatrixₗ.symm M‖
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial k = 0 ↔ n < k
  | 0 => by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
  | succ k => by
    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
    exact fun h _ => h

Proof state:
n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
  Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]

Result:
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k

Proof state:
n : ℕ
⊢ n.descFactorial 0 = 0 ↔ n < 0

Tactic:
simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]

Result:
no goals

Proof state:
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k

Tactic:
exact fun h _ => h

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_le_dom {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁)
    (h₂ : Continuous[t₁, t₃] f) : Continuous[t₂, t₃] f

Proof state:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous f
⊢ Continuous f

Tactic:
rw [continuous_iff_le_induced] at h₂ ⊢

Result:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃

Proof state:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃

Tactic:
exact le_trans h₁ h₂

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_pow {x : ℝ≥0∞} {n : ℕ} : log (x ^ n) = n * log x

Proof state:
case inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
⊢ (x ^ n).log = ↑n * x.log

Tactic:
rcases ENNReal.trichotomy x with (rfl | rfl | x_real)

Result:
case inr.inl
n : ℕ
n_pos : n > 0
⊢ (0 ^ n).log = ↑n * log 0

case inr.inr.inl
n : ℕ
n_pos : n > 0
⊢ (⊤ ^ n).log = ↑n * ⊤.log

case inr.inr.inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
x_real : 0 < x.toReal
⊢ (x ^ n).log = ↑n * x.log

Proof state:
case inr.inl
n : ℕ
n_pos : n > 0
⊢ (0 ^ n).log = ↑n * log 0

Tactic:
rw [zero_pow n_pos.ne', log_zero, EReal.mul_bot_of_pos (Nat.cast_pos'.2 n_pos)]

Result:
no goals

Proof state:
case inr.inr.inl
n : ℕ
n_pos : n > 0
⊢ (⊤ ^ n).log = ↑n * ⊤.log

Tactic:
rw [ENNReal.top_pow n_pos, log_top, EReal.mul_top_of_pos (Nat.cast_pos'.2 n_pos)]

Result:
no goals

Proof state:
case inr.inr.inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
x_real : 0 < x ∧ x < ⊤
⊢ (x ^ n).log = ↑n * x.log

Tactic:
simp only [log, pow_eq_zero_iff', x_real.1.ne', false_and, ↓reduceIte, pow_eq_top_iff,
  x_real.2.ne, toReal_pow, Real.log_pow, EReal.coe_mul, EReal.coe_coe_eq_natCast]

Result:
no goals

Proof state:
case inr.inr.inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
x_real : 0 < x.toReal
⊢ (x ^ n).log = ↑n * x.log

Tactic:
replace x_real := ENNReal.toReal_pos_iff.1 x_real

Result:
case inr.inr.inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
x_real : 0 < x ∧ x < ⊤
⊢ (x ^ n).log = ↑n * x.log

Proof state:
case inl
x : ℝ≥0∞
n : ℕ
n_zero : n = 0
⊢ (x ^ n).log = ↑n * x.log

Tactic:
simp [n_zero, pow_zero x]

Result:
no goals

Proof state:
x : ℝ≥0∞
n : ℕ
⊢ (x ^ n).log = ↑n * x.log

Tactic:
rcases Nat.eq_zero_or_pos n with n_zero | n_pos

Result:
case inl
x : ℝ≥0∞
n : ℕ
n_zero : n = 0
⊢ (x ^ n).log = ↑n * x.log

case inr
x : ℝ≥0∞
n : ℕ
n_pos : n > 0
⊢ (x ^ n).log = ↑n * x.log
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem bitwise_div_two_pow (of_false_false : f false false = false

Proof state:
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ bitwise f x y / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat), (bitwise f x y / 2 ^ n).testBit i = (bitwise f (x / 2 ^ n) (y / 2 ^ n)).testBit i

Proof state:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat), (bitwise f x y / 2 ^ n).testBit i = (bitwise f (x / 2 ^ n) (y / 2 ^ n)).testBit i

Tactic:
simp [testBit_bitwise of_false_false, testBit_div_two_pow]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_iff_ringHom_rangeS (p : S[X]) : p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS

Tactic:
simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]

Result:
no goals