harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem norm_condExpL2_coe_le (hm : m ≤ m0) (f : α →₂[μ] E) :
    ‖(condExpL2 E 𝕜 hm f : α →₂[μ] E)‖ ≤ ‖f‖

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ (eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ).toReal ≤ (eLpNorm (↑↑f) 2 μ).toReal

Tactic:
exact ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) (eLpNorm_condExpL2_le hm f)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ ‖↑((condExpL2 E 𝕜 hm) f)‖ ≤ ‖f‖

Tactic:
rw [Lp.norm_def, Lp.norm_def]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ (eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ).toReal ≤ (eLpNorm (↑↑f) 2 μ).toReal
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem orthogonalComplement_iSup_eigenspaces (hT : T.IsSymmetric) (μ : 𝕜) :
    eigenspace (T.restrict hT.orthogonalComplement_iSup_eigenspaces_invariant) μ = ⊥

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Tactic:
refine eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant ?_

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
⊢ Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ

Tactic:
exact H₂.disjoint

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Tactic:
set p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
⊢ Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ

Tactic:
have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Irreducible.not_square (ha : Irreducible a) : ¬IsSquare a

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
ha : Irreducible a
⊢ ¬IsSquare a

Tactic:
rw [isSquare_iff_exists_sq]

Result:
M : Type u_1
inst✝ : CommMonoid M
a : M
ha : Irreducible a
⊢ ¬∃ r, a = r ^ 2

Proof state:
M : Type u_1
inst✝ : CommMonoid M
b : M
ha : Irreducible (b ^ 2)
⊢ 2 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
ha : Irreducible a
⊢ ¬∃ r, a = r ^ 2

Tactic:
rintro ⟨b, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
b : M
ha : Irreducible (b ^ 2)
⊢ False

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
b : M
ha : Irreducible (b ^ 2)
⊢ False

Tactic:
exact not_irreducible_pow (by decide) ha

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biproductComparison'_comp_biproductComparison :
    biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)

Proof state:
case w.w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
j✝¹ j✝ : J
⊢ biproduct.ι (F.obj ∘ f) j✝ ≫ (F.biproductComparison' f ≫ F.biproductComparison f) ≫ biproduct.π (F.obj ∘ f) j✝¹ =
    biproduct.ι (F.obj ∘ f) j✝ ≫ 𝟙 (⨁ F.obj ∘ f) ≫ biproduct.π (F.obj ∘ f) j✝¹

Tactic:
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)

Tactic:
classical
  ext
  simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)

Tactic:
ext

Result:
case w.w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
j✝¹ j✝ : J
⊢ biproduct.ι (F.obj ∘ f) j✝ ≫ (F.biproductComparison' f ≫ F.biproductComparison f) ≫ biproduct.π (F.obj ∘ f) j✝¹ =
    biproduct.ι (F.obj ∘ f) j✝ ≫ 𝟙 (⨁ F.obj ∘ f) ≫ biproduct.π (F.obj ∘ f) j✝¹
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem _root_.Finset.coe_infsep [DecidableEq α] (s : Finset α) : (s : Set α).infsep =
    if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
⊢ (↑s).Nontrivial ↔ s.offDiag.Nonempty

Tactic:
rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
⊢ (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Tactic:
split_ifs with hs

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0

Tactic:
exact (not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
⊢ (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Tactic:
have H : (s : Set α).Nontrivial ↔ s.offDiag.Nonempty := by
  rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]

Result:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
⊢ (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sign_mul_inv_abs (a : EReal) : (sign a) * (a.abs : EReal)⁻¹ = a⁻¹

Proof state:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]

Result:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑|a|)⁻¹ = (↑a)⁻¹

Proof state:
case h_real
a : ℝ
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)

Result:
case h_real.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

case h_real.inr.inl

⊢ ↑(sign ↑0) * (↑(↑0).abs)⁻¹ = (↑0)⁻¹

case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Proof state:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑|a|)⁻¹ = (↑a)⁻¹

Tactic:
congr

Result:
case h_real.inr.inr.e_a.e_a
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Proof state:
case h_real.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a,
  coe_ennreal_ofReal, max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]

Result:
no goals

Proof state:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]

Result:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Proof state:
case h_real.inr.inl

⊢ ↑(sign ↑0) * (↑(↑0).abs)⁻¹ = (↑0)⁻¹

Tactic:
rw [coe_zero, sign_zero, SignType.coe_zero, abs_zero, coe_ennreal_zero, inv_zero, mul_zero]

Result:
no goals

Proof state:
case h_top

⊢ ↑(sign ⊤) * (↑⊤.abs)⁻¹ = ⊤⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h_real.inr.inr.e_a.e_a
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Tactic:
exact abs_of_pos a_pos

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_Iio : #(Iio b) = b

Proof state:
b : ℕ
⊢ #(Iio b) = b

Tactic:
rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem coeff_iterate_fslope (k n : ℕ) : (fslope^[k] p).coeff n = p.coeff (n + k)

Proof state:
case zero
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ (fslope^[0] p).coeff n = p.coeff (n + 0)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
k n : ℕ
⊢ (fslope^[k] p).coeff n = p.coeff (n + k)

Tactic:
induction k generalizing p with
| zero => rfl
| succ k ih => simp [ih, add_assoc]

Result:
no goals

Proof state:
case succ
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n k : ℕ
ih : ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E}, (fslope^[k] p).coeff n = p.coeff (n + k)
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ (fslope^[k + 1] p).coeff n = p.coeff (n + (k + 1))

Tactic:
simp [ih, add_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem odd_length : Odd (ℓ t)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ cs.lengthParity t = Multiplicative.ofAdd 1

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.lengthParity (w * cs.simple i * w⁻¹) = Multiplicative.ofAdd 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ Odd (cs.length t)

Tactic:
suffices cs.lengthParity t = Multiplicative.ofAdd 1 by
  simpa [lengthParity_eq_ofAdd_length, ZMod.eq_one_iff_odd]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ cs.lengthParity t = Multiplicative.ofAdd 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
this : cs.lengthParity t = Multiplicative.ofAdd 1
⊢ Odd (cs.length t)

Tactic:
simpa [lengthParity_eq_ofAdd_length, ZMod.eq_one_iff_odd]

Result:
no goals

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.lengthParity (w * cs.simple i * w⁻¹) = Multiplicative.ofAdd 1

Tactic:
simp [lengthParity_simple]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem toPlus_naturality {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
    η ≫ J.toPlus Q = J.toPlus _ ≫ J.plusMap η

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ η.app x✝ ≫
      Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯ ≫
        colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫
      (J.diagramNatTrans η (unop x✝)).app (op ⊤) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤)

Tactic:
simp_rw [← Category.assoc]

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ (η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I => Q.map I.f.op) ⋯) ≫
      colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I => P.map I.f.op) ⋯ ≫
        (J.diagramNatTrans η (unop x✝)).app (op ⊤)) ≫
      colimit.ι (J.diagram Q (unop x✝)) (op ⊤)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
I : ⊤.shape.L
⊢ (η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj x✝) (fun I => Q.map I.f.op) ⋯) ≫ Multiequalizer.ι (⊤.index Q) I =
    (Multiequalizer.lift (⊤.index P) (P.obj x✝) (fun I => P.map I.f.op) ⋯ ≫
        Multiequalizer.lift (⊤.index Q) (multiequalizer (⊤.index P))
          (fun x => Multiequalizer.ι (⊤.index P) x ≫ η.app (op x.Y)) ⋯) ≫
      Multiequalizer.ι (⊤.index Q) I

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_eval_neBot_iff' {ι : Type*} {α : ι → Type*} {i : ι} {f : Filter (α i)} :
    (comap (eval i) f).NeBot ↔ (∀ j, Nonempty (α j)) ∧ NeBot f

Proof state:
case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, *]

Result:
no goals

Proof state:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬⊥.NeBot ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ f.NeBot)

Tactic:
simp [← Classical.nonempty_pi]

Result:
no goals

Proof state:
case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H

Result:
case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Proof state:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Result:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬⊥.NeBot ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ f.NeBot)

Proof state:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty (∀ j, α j) with H | H

Result:
case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
-- Mathlib/Topology/Constructions.lean
theorem DenseRange.prodMap {ι : Type*} {κ : Type*} {f : ι → Y} {g : κ → Z} (hf : DenseRange f)
    (hg : DenseRange g) : DenseRange (Prod.map f g)

Proof state:
Y : Type v
Z : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
ι : Type u_5
κ : Type u_6
f : ι → Y
g : κ → Z
hf : DenseRange f
hg : DenseRange g
⊢ DenseRange (Prod.map f g)

Tactic:
simpa only [DenseRange, prod_range_range_eq] using hf.prod hg

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b)
    (n : ℕ) (f : R[A]) : (f ^ n).support.sup degb ≤ n • f.support.sup degb

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum

Tactic:
refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.map (fun f => f.support.sup degb) (List.replicate n f)).sum = (List.replicate n (f.support.sup degb)).sum

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).support.sup degb ≤ n • f.support.sup degb

Tactic:
rw [← List.prod_replicate, ← List.sum_replicate]

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.map (fun f => f.support.sup degb) (List.replicate n f)).sum = (List.replicate n (f.support.sup degb)).sum

Tactic:
rw [List.map_replicate]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_iff_comp_left (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] [∀ i, M.HasHomology i]
    [hφ : QuasiIso φ] :
    QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ'

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_comp_left φ φ']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem one_eq_zero_iff : 1#w = 0#w ↔ w = 0

Proof state:
w : Nat
⊢ 1#w = 0#w ↔ w = 0

Tactic:
constructor

Result:
case mp
w : Nat
⊢ 1#w = 0#w → w = 0

case mpr
w : Nat
⊢ w = 0 → 1#w = 0#w

Proof state:
case mp.succ
n✝ : Nat
h : (1#(n✝ + 1)).toNat = (0#(n✝ + 1)).toNat
⊢ n✝ + 1 = 0

Tactic:
simp at h

Result:
no goals

Proof state:
case mpr
w : Nat
⊢ w = 0 → 1#w = 0#w

Tactic:
rintro rfl

Result:
case mpr

⊢ 1#0 = 0#0

Proof state:
case mp.zero
h : 1#0 = 0#0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case mpr

⊢ 1#0 = 0#0

Tactic:
simp

Result:
no goals

Proof state:
case mp.succ
n✝ : Nat
h : 1#(n✝ + 1) = 0#(n✝ + 1)
⊢ n✝ + 1 = 0

Tactic:
replace h := congrArg BitVec.toNat h

Result:
case mp.succ
n✝ : Nat
h : (1#(n✝ + 1)).toNat = (0#(n✝ + 1)).toNat
⊢ n✝ + 1 = 0

Proof state:
case mp
w : Nat
h : 1#w = 0#w
⊢ w = 0

Tactic:
cases w

Result:
case mp.zero
h : 1#0 = 0#0
⊢ 0 = 0

case mp.succ
n✝ : Nat
h : 1#(n✝ + 1) = 0#(n✝ + 1)
⊢ n✝ + 1 = 0

Proof state:
case mp
w : Nat
⊢ 1#w = 0#w → w = 0

Tactic:
intro h

Result:
case mp
w : Nat
h : 1#w = 0#w
⊢ w = 0
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem inducedOuterMeasure_preimage (f : α ≃ α) (Pm : ∀ s : Set α, P (f ⁻¹' s) ↔ P s)
    (mm : ∀ (s : Set α) (hs : P s), m (f ⁻¹' s) ((Pm _).mpr hs) = m s hs) {A : Set α} :
    inducedOuterMeasure m P0 m0 (f ⁻¹' A) = inducedOuterMeasure m P0 m0 A

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
hs : P s
⊢ ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s hs

Tactic:
refine iInf_congr_Prop f.surjective.preimage_subset_preimage_iff ?_

Result:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
hs : P s
⊢ A ⊆ s → m (⇑f ⁻¹' s) ⋯ = m s hs