harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_iff_emultiplicity_le_one [CommMonoid R] (r : R) :
    Squarefree r ↔ ∀ x : R, emultiplicity x r ≤ 1 ∨ IsUnit x

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ↑2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
norm_cast

Result:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r : R
⊢ Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x

Tactic:
refine forall_congr' fun a => ?_

Result:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 1 + 1 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
exact Order.add_one_le_iff_of_not_isMax (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
rw [← one_add_one_eq_two]

Result:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 1 + 1 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a

Tactic:
rw [← sq, pow_dvd_iff_le_emultiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]

Result:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ↑2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Proof state:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ¬IsMax 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0) : LinearIndependent 𝕜 f

Proof state:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
⊢ LinearIndependent 𝕜 f

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : IsEmpty ι
⊢ LinearIndependent 𝕜 f

case inr
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : Nonempty ι
⊢ LinearIndependent 𝕜 f

Proof state:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : Nonempty ι
⊢ Pairwise fun k₁ k₂ => wInner 1 (f k₁) (f k₂) = 0

Tactic:
simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

Result:
no goals

Proof state:
case inl
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : IsEmpty ι
⊢ LinearIndependent 𝕜 f

Tactic:
have : IsEmpty κ := ⟨fun k ↦ hf k <| Subsingleton.elim ..⟩

Result:
case inl
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : IsEmpty ι
this : IsEmpty κ
⊢ LinearIndependent 𝕜 f

Proof state:
case inl
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : IsEmpty ι
this : IsEmpty κ
⊢ LinearIndependent 𝕜 f

Tactic:
exact linearIndependent_empty_type

Result:
no goals

Proof state:
case inr
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner cWeight (f k₁) (f k₂) = 0
h✝ : Nonempty ι
⊢ LinearIndependent 𝕜 f

Tactic:
exact linearIndependent_of_ne_zero_of_wInner_one_eq_zero hf <| by
  simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem iSup_lintegral_measurable_le_eq_lintegral (f : α → ℝ≥0∞) :
    ⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ a, g a ∂μ = ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ

Tactic:
refine iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : ⇑i ≤ fun a => f a
⊢ i.lintegral μ ≤ ∫⁻ (a : α), i a ∂μ

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : ⇑i ≤ fun a => f a
⊢ i.lintegral μ ≤ ∫⁻ (a : α), i a ∂μ

Tactic:
exact le_of_eq (i.lintegral_eq_lintegral _).symm

Result:
no goals

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral]

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/MidpointZero.lean
theorem lineMap_one_half {R : Type*} {V P : Type*} [DivisionRing R] [CharZero R] [AddCommGroup V]
    [Module R V] [AddTorsor V P] (a b : P) : lineMap a b (1 / 2 : R) = midpoint R a b

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
a b : P
⊢ (lineMap a b) (1 / 2) = midpoint R a b

Tactic:
rw [one_div, lineMap_inv_two]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_le_one : #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Proof state:
case inr.intro.refine_1
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
rintro ⟨y, rfl⟩

Result:
case inr.intro.refine_1.intro
α : Type u_1
x y : α
hx : x ∈ {y}
⊢ ∀ a ∈ {y}, ∀ b ∈ {y}, a = b

Proof state:
case inr.intro
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).le_iff_eq.trans (card_eq_one.trans ⟨?_, ?_⟩)

Result:
case inr.intro.refine_1
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b

case inr.intro.refine_2
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}

Proof state:
case inr.intro.refine_2
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}

Tactic:
exact fun h => ⟨x, eq_singleton_iff_unique_mem.2 ⟨hx, fun y hy => h _ hy _ hx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_1
⊢ #∅ ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b

case inr.intro
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Proof state:
case inr.intro.refine_1.intro
α : Type u_1
x y : α
hx : x ∈ {y}
⊢ ∀ a ∈ {y}, ∀ b ∈ {y}, a = b

Tactic:
simp

Result:
no goals

Proof state:
case inl
α : Type u_1
⊢ #∅ ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma hasSmallLocalizedHom_iff_target {Y Y' : C} (f : Y ⟶  Y') (hf : W f):
    HasSmallLocalizedHom.{w} W X Y ↔ HasSmallLocalizedHom.{w} W X Y'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')

Tactic:
exact small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

Result:
no goals
-- Mathlib/Topology/Ultrafilter.lean
theorem mem_closure_iff_ultrafilter :
    x ∈ closure s ↔ ∃ u : Ultrafilter X, s ∈ u ∧ ↑u ≤ 𝓝 x

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x

Tactic:
simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_two_two_eq_four (n : ℕ) : hyperoperation (n + 1) 2 2 = 4

Proof state:
n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4

Tactic:
induction' n with nn nih

Result:
case zero

⊢ hyperoperation (0 + 1) 2 2 = 4

case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (nn + 1 + 1) 2 2 = 4

Proof state:
case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (nn + 1 + 1) 2 2 = 4

Tactic:
rw [hyperoperation_recursion, hyperoperation_ge_two_eq_self, nih]

Result:
no goals

Proof state:
case zero

⊢ hyperoperation (0 + 1) 2 2 = 4

Tactic:
rw [hyperoperation_one]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem one_comul (M : Bimon_ C) :
    M.X.one ≫ M.comul.hom = (λ_ _).inv ≫ (M.X.one ⊗ M.X.one)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.X.one ≫ M.comul.hom = (λ_ (𝟙_ C)).inv ≫ (M.X.one ⊗ M.X.one)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma mu_mul_zeta : (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
congr! with x hx

Result:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (mu 𝕜) a x * (zeta 𝕜) x b = (mu 𝕜) a x

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = 1 a b

Tactic:
calc
  _ = ∑ x ∈ Icc a b, mu 𝕜 a x := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]
  _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu_right ..

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
⊢ mu 𝕜 * zeta 𝕜 = 1

Tactic:
ext a b

Result:
case h
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = 1 a b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
rw [mul_apply]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Proof state:
case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (mu 𝕜) a x * (zeta 𝕜) x b = (mu 𝕜) a x

Tactic:
simp [(mem_Icc.1 hx).2]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
lemma getElem_leftInvSeq (ω : List B) (j : ℕ) (h : j < ω.length) :
    (lis ω)[j]'(by simp[h]) =
    cs.wordProd (List.take j ω) * s ω[j] * (cs.wordProd (List.take j ω))⁻¹

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ j < (cs.leftInvSeq ω).length

Tactic:
simp[h]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ =
    cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹

Tactic:
simp [h]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.leftInvSeq ω)[j] = cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹

Tactic:
rw [← List.getD_eq_getElem (lis ω) 1, getD_leftInvSeq]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ =
    cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_zmod_cast (a : ZMod n) : ((cast a : ℤ) : ZMod n) = a

Proof state:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑↑a.val = a

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Tactic:
dsimp [ZMod.cast]

Result:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑↑a.val = a

Proof state:
n : ℕ
a : ZMod n
⊢ ↑a.cast = a

Tactic:
cases n

Result:
case zero
a : ZMod 0
⊢ ↑a.cast = a

case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Proof state:
case zero
a : ZMod 0
⊢ ↑a.cast = a

Tactic:
simp [ZMod.cast, ZMod]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_singleton (a : α) : ({a} : Set α).offDiag = ∅

Proof state:
α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem aemeasurable_toNNReal_abs_det_fderivWithin (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => (f' x).det) (μ.restrict s)

Tactic:
refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable f' (μ.restrict s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)

Tactic:
apply measurable_real_toNNReal.comp_aemeasurable

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => |(f' x).det|) (μ.restrict s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
exact aemeasurable_fderivWithin μ hs hf'

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => |(f' x).det|) (μ.restrict s)

Tactic:
refine continuous_abs.measurable.comp_aemeasurable ?_

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => (f' x).det) (μ.restrict s)
-- Mathlib/Algebra/Algebra/Operations.lean
theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n

Proof state:
case zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
h : 0 ≠ 0
⊢ (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0

Tactic:
exact (h rfl).elim

Result:
no goals

Proof state:
case succ.succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n + 1 ≠ 0 → (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid

Tactic:
rw [ih n.succ_ne_zero]

Result:
no goals

Proof state:
case succ.zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ (M ^ 0).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ 0 * M.toAddSubmonoid

Tactic:
rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)

Tactic:
rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]

Result:
case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid

Proof state:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n

Tactic:
induction n with
| zero => exact (h rfl).elim
| succ n ih =>
  rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
  cases n with
  | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
  | succ n => rw [ih n.succ_ne_zero]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid

Tactic:
cases n with
| zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
| succ n => rw [ih n.succ_ne_zero]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_lt_two : φ < 2

Proof state:
⊢ φ < 2

Tactic:
calc
(1 + sqrt 5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
_ = 2 := by norm_num

Result:
no goals

Proof state:
⊢ (1 + 3) / 2 = 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h.bc

⊢ √5 < 3

Tactic:
rw [sqrt_lt'] <;> norm_num

Result:
no goals

Proof state:
⊢ (1 + √5) / 2 < (1 + 3) / 2

Tactic:
gcongr

Result:
case h.bc

⊢ √5 < 3