harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma isDiameter_iff_mem_and_mem_and_wbtw :
    s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ p₂ = 2 * s.radius
⊢ s.IsDiameter p₁ p₂

Tactic:
exact isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Tactic:
refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
⊢ s.IsDiameter p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ s.center + dist s.center p₂ = dist p₁ p₂
⊢ s.IsDiameter p₁ p₂

Tactic:
rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ p₂ = 2 * s.radius
⊢ s.IsDiameter p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
⊢ s.IsDiameter p₁ p₂

Tactic:
have hd := hr.dist_add_dist

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : Wbtw ℝ p₁ s.center p₂
hd : dist p₁ s.center + dist s.center p₂ = dist p₁ p₂
⊢ s.IsDiameter p₁ p₂
-- Mathlib/Data/List/Basic.lean
theorem foldrM_eq_foldr (f : α → β → m β) (b l) :
    foldrM f b l = foldr (fun a mb => mb >>= f a) (pure b) l

Proof state:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun a mb => mb >>= f a) (pure b) l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_sum_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => degreeOf i (f j)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => degreeOf i (f j)

Tactic:
simp_rw [degreeOf_eq_sup]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ j ∈ s, f j).support.sup fun m => m i) ≤ s.sup fun j => (f j).support.sup fun m => m i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ j ∈ s, f j).support.sup fun m => m i) ≤ s.sup fun j => (f j).support.sup fun m => m i

Tactic:
exact supDegree_sum_le

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpen_prod_iff {s : Set (X × Y)} :
    IsOpen s ↔ ∀ a b, (a, b) ∈ s →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s :=
  isOpen_iff_mem_nhds.trans <| by simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma le_max_right (a b : α) : b ≤ max a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ b ≤ max a b

Tactic:
simp [max_def, if_pos h, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ max a b

Tactic:
if h : a ≤ b
then simp [max_def, if_pos h, le_refl]
else simpa [max_def, if_neg h] using le_of_not_le h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ max a b

Tactic:
simpa [max_def, if_neg h] using le_of_not_le h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id

Proof state:
α : Type u
⊢ Option.map id = id

Tactic:
funext

Result:
case h
α : Type u
x✝ : Option α
⊢ Option.map id x✝ = id x✝

Proof state:
case h
α : Type u
x✝ : Option α
⊢ Option.map id x✝ = id x✝

Tactic:
simp [map_id]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem to_real_re (x : ℤ[i]) : ((x.re : ℤ) : ℝ) = (x : ℂ).re

Proof state:
x : ℤ[i]
⊢ ↑x.re = (toComplex x).re

Tactic:
simp [toComplex_def]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₁Γ₀_hom_app_f_f (K : ChainComplex C ℕ) (n : ℕ) :
    (N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ (N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

Tactic:
rw [N₁Γ₀_hom_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

Tactic:
apply comp_id

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
/-- If `φ : a ⟶ b` lifts `f` and `ψ : b ⟶ c` lifts `𝟙 T`, then `φ ≫ ψ` lifts `f` -/
lemma comp_lift_id_right' {R S : 𝒮} {a b c : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
    (T : 𝒮) (ψ : b ⟶ c) [p.IsHomLift (𝟙 T) ψ] : p.IsHomLift f (φ ≫ ψ)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ S = T

Tactic:
rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 S) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 S) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem dist_orthocenter_reflection_circumcenter_finset (t : Triangle ℝ P) {i₁ i₂ : Fin 3}
    (h : i₁ ≠ i₂) :
    dist t.orthocenter
        (reflection (affineSpan ℝ (t.points '' ↑({i₁, i₂} : Finset (Fin 3)))) t.circumcenter) =
      t.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (circumcenter t)) =
    circumradius t

Tactic:
simp only [mem_singleton, coe_insert, coe_singleton, Set.mem_singleton_iff]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) =
    circumradius t

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) =
    circumradius t

Tactic:
exact dist_orthocenter_reflection_circumcenter _ h

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_empty_right (t s : Set α) : t.ite s ∅ = s ∩ t

Proof state:
α : Type u
t s : Set α
⊢ t.ite s ∅ = s ∩ t

Tactic:
simp [Set.ite]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_of_X_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W'.addZ P Q = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| mul_ne_zero hPz hQz

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q * (P z * Q z) = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q * (P z * Q z) = 0

Tactic:
rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isRightDescent_one (i : B) : ¬cs.IsRightDescent 1 i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ ¬cs.IsRightDescent 1 i

Tactic:
simp [IsRightDescent]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem isClosed_setOf_inseparable : IsClosed { p : X × X | Inseparable p.1 p.2 }

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ IsClosed {p | Inseparable p.1 p.2}

Tactic:
simp only [← specializes_iff_inseparable, isClosed_setOf_specializes]

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
/-- A zigzag in a discrete category entails an equality of its extremities -/
lemma eq_of_zigzag (X) {a b : Discrete X} (h : Zigzag a b) : a.as = b.as

Proof state:
case refl
X : Type u_1
a b : Discrete X
⊢ a.as = a.as

Tactic:
rfl

Result:
no goals

Proof state:
case tail
X : Type u_1
a b b✝ c✝ : Discrete X
a✝ : Relation.ReflTransGen Zag a b✝
h : Zag b✝ c✝
eq : a.as = b✝.as
⊢ a.as = c✝.as

Tactic:
exact eq.trans (eq_of_zag _ h)

Result:
no goals

Proof state:
X : Type u_1
a b : Discrete X
h : Zigzag a b
⊢ a.as = b.as

Tactic:
induction h with
| refl => rfl
| tail _ h eq  => exact eq.trans (eq_of_zag _ h)

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem isClosed_iff {s : Set Γ₀} : IsClosed s ↔ (0 : Γ₀) ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici,
  compl_subset_compl]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul : a / b * c = a / (b / c)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a / (b / c)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem pow_apply_mem_toList_iff_mem_support {n : ℕ} : (p ^ n) x ∈ p.toList x ↔ x ∈ p.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ p.support → p.SameCycle x ((p ^ n) x)

Tactic:
refine fun _ => SameCycle.symm ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
x✝ : x ∈ p.support
⊢ p.SameCycle ((p ^ n) x) x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ (p ^ n) x ∈ p.toList x ↔ x ∈ p.support

Tactic:
rw [mem_toList_iff, and_iff_right_iff_imp]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ p.support → p.SameCycle x ((p ^ n) x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
x✝ : x ∈ p.support
⊢ p.SameCycle ((p ^ n) x) x

Tactic:
rw [sameCycle_pow_left]

Result:
no goals
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem norm_deriv_le_one_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R))
    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (h₀ : 0 < R) : ‖deriv f c‖ ≤ 1 :=
  (norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')

Proof state:
f : ℂ → ℂ
c : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
h₀ : 0 < R
⊢ MapsTo f (ball c R) (ball (f c) R)

Tactic:
rwa [hc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem Basis.addHaar_eq_iff [SecondCountableTopology E] (b : Basis ι ℝ E) (μ : Measure E)
    [SigmaFinite μ] [IsAddLeftInvariant μ] :
    b.addHaar = μ ↔ μ b.parallelepiped = 1

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ addHaarMeasure b.parallelepiped = μ ↔ μ ↑b.parallelepiped = 1

Tactic:
exact addHaarMeasure_eq_iff b.parallelepiped μ

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ b.addHaar = μ ↔ μ ↑b.parallelepiped = 1

Tactic:
rw [Basis.addHaar_def]

Result:
ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ addHaarMeasure b.parallelepiped = μ ↔ μ ↑b.parallelepiped = 1
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Hom.cast_cast {u v u' v' u'' v'' : U} (e : u ⟶ v) (hu : u = u') (hv : v = v')
    (hu' : u' = u'') (hv' : v' = v'') :
    (e.cast hu hv).cast hu' hv' = e.cast (hu.trans hu') (hv.trans hv')

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ e

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
e : u'' ⟶ v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ e) = cast ⋯ ⋯ e

Proof state:
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
e : u'' ⟶ v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ e) = cast ⋯ ⋯ e

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma one_le_netMaxcard_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    1 ≤ netMaxcard T F U n ↔ F.Nonempty

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F ≠ ∅

Tactic:
exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty

Tactic:
rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F ≠ ∅
-- Mathlib/Dynamics/Ergodic/Conservative.lean
theorem id (μ : Measure α) : Conservative id μ :=
  { toQuasiMeasurePreserving := QuasiMeasurePreserving.id μ
    exists_mem_iterate_mem' := fun _ _ h0 => by
      simpa [exists_ne] using nonempty_of_measure_ne_zero h0 }

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
x✝¹ : Set α
x✝ : MeasurableSet x✝¹
h0 : μ x✝¹ ≠ 0
⊢ ∃ x ∈ x✝¹, ∃ m, m ≠ 0 ∧ id^[m] x ∈ x✝¹

Tactic:
simpa [exists_ne] using nonempty_of_measure_ne_zero h0

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_inv (μ : Measure G) [IsInvInvariant μ] (A : Set G) : μ A⁻¹ = μ A

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsInvInvariant
A : Set G
⊢ μ A⁻¹ = μ A

Tactic:
rw [← inv_apply, inv_eq_self]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Topology.IsInducing.r0Space [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) :
    R0Space Y where
  specializes_symmetric a b

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : R0Space X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ a ⤳ b → b ⤳ a

Tactic:
simpa only [← hf.specializes_iff] using Specializes.symm

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Quotient.lean
theorem polynomialQuotientEquivQuotientPolynomial_symm_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial.symm (Quotient.mk _ f) = f.map (Quotient.mk I)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f) = Polynomial.map (Quotient.mk I) f

Tactic:
rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk,
  Equiv.coe_fn_mk, Quotient.lift_mk, coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map,
  ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem valid : ∀ {s}, ValidFor l m r s → Valid s
  | _, ⟨⟩ => ⟨⟨l, m ++ r, by simp⟩, ⟨l ++ m, r, by simp⟩, Nat.le_add_right ..⟩

Proof state:
l m r : List Char
⊢ l ++ (m ++ r) =
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.str.data ∧
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.startPos.byteIdx =
      utf8Len l

Tactic:
simp

Result:
no goals

Proof state:
l m r : List Char
⊢ l ++ m ++ r =
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.str.data ∧
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.stopPos.byteIdx =
      utf8Len (l ++ m)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDeriv_comp_sub' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x - a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z => f (z - a)) = fun x => iteratedFDeriv 𝕜 n f (x - a)

Tactic:
simpa [sub_eq_add_neg] using iteratedFDeriv_comp_add_right' n (-a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
    k ∈ insertManyIfNewUnit m l → k ∈ m

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
contains_eq_false : l.contains k = false
⊢ (insertManyIfNewUnit m l).contains k = true → m.contains k = true

Tactic:
simp_to_raw using Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
contains_eq_false : l.contains k = false
⊢ k ∈ insertManyIfNewUnit m l → k ∈ m

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
contains_eq_false : l.contains k = false
⊢ (insertManyIfNewUnit m l).contains k = true → m.contains k = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_le_size : countP p l ≤ l.size

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).size ≤ l.size

Tactic:
apply size_filter_le

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p l ≤ l.size

Tactic:
simp only [countP_eq_size_filter]

Result:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).size ≤ l.size
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem boundary_zero : c.boundary 0 = 0

Proof state:
n : ℕ
c : Composition n
⊢ c.boundary 0 = 0

Tactic:
simp [boundary, Fin.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem?_eraseIdx_of_ge (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : i ≤ j) :
    (l.eraseIdx i)[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : i ≤ j
⊢ (l.eraseIdx i h)[j]? = l[j + 1]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?

Tactic:
simp only [dite_eq_ite, ite_eq_right_iff]

Result:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?

Tactic:
intro h'

Result:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h'✝ : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h'✝ : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Unramified/Finite.lean
lemma one_tmul_mul_elem
    (s : S) : (1 ⊗ₜ s) * elem R S = (s ⊗ₜ 1) * elem R S

Proof state:
R : Type u_3
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
s : S
⊢ 1 ⊗ₜ[R] s * elem R S = s ⊗ₜ[R] 1 * elem R S

Tactic:
rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]

Result:
no goals