harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Field.lean
theorem IsPreconnected.eq_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S)
    (hsq : EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) {y : α} (hy : y ∈ S)
    (hy' : f y = g y) : EqOn f g S := fun x hx => by
  rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
  · exact h hx
  · rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption

Proof state:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
⊢ f x = g x

Tactic:
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)

Result:
case inl
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x

case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Proof state:
case inl
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x

Tactic:
exact h hx

Result:
no goals

Proof state:
case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Tactic:
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
  (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_prime_pow_eq_geom_sum {R : Type*} [CommRing R] {p n : ℕ} (hp : p.Prime) :
    cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ n) ^ i

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n) ^ i

Tactic:
have : ∀ m, (cyclotomic (p ^ (m + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) ↔
    ((∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) *
      ∏ x ∈ Finset.range (m + 1), cyclotomic (p ^ x) R) = X ^ p ^ (m + 1) - 1 := by
  intro m
  have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
    (pow_pos hp.pos (m + 1))
  rw [eq_comm] at this
  rw [this, Nat.prod_properDivisors_prime_pow hp]

Result:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n) ^ i

Proof state:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  ∑ i ∈ range p, (X ^ p ^ m) ^ i = cyclotomic (p ^ (m + 1)) R ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Tactic:
rw [eq_comm] at this

Result:
R : Type u_1
inst✝ : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R = X ^ p ^ (m + 1) - 1
⊢ cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
    (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : cyclotomic (p ^ (n_n + 1)) R = ∑ i ∈ range p, (X ^ p ^ n_n) ^ i
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
rw [this] at n_ih

Result:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) *
      ((∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) * ∑ i ∈ range p, (X ^ p ^ n_n) ^ i) =
    X ^ p ^ (n_n + 1 + 1) - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h)

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).head h = (head✝ :: tail✝)[0]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ l.head h = l[0]

Tactic:
cases l with
| nil => simp at h
| cons _ _ => simp

Result:
no goals

Proof state:
case nil
α : Type u_1
h : [] ≠ []
⊢ [].head h = [][0]

Tactic:
simp at h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.emetric_ball_nnreal {x : α} {ε : ℝ≥0} : EMetric.ball x ε = ball x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = EMetric.ball x (ENNReal.ofReal ↑ε)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = ball x ↑ε

Tactic:
rw [← Metric.emetric_ball]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = EMetric.ball x (ENNReal.ofReal ↑ε)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem reverse_iota : reverse (iota n) = range' 1 n

Proof state:
case succ
n : Nat
ih : (iota n).reverse = range' 1 n
⊢ (iota (n + 1)).reverse = range' 1 (n + 1)

Tactic:
rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]

Result:
no goals

Proof state:
n : Nat
⊢ (iota n).reverse = range' 1 n

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]

Result:
no goals

Proof state:
case zero

⊢ (iota 0).reverse = range' 1 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma isIso_opcyclesMap'_of_isIso_of_epi (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁)
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    IsIso (opcyclesMap' φ h₁ h₂)

Proof state:
case refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0

Tactic:
simp only [← cancel_epi φ.τ₁, comp_zero, φ.comm₁₂_assoc, IsIso.hom_inv_id_assoc, h₁.wp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ IsIso (opcyclesMap' φ h₁ h₂)

Tactic:
refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩

Result:
case refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0

case refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?refine_1 = 𝟙 h₁.Q

case refine_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?refine_1 ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q

Proof state:
case refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ = 𝟙 h₁.Q

Tactic:
simp only [← cancel_epi h₁.p, p_opcyclesMap'_assoc, h₂.p_descQ,
  IsIso.hom_inv_id_assoc, comp_id]

Result:
no goals

Proof state:
case refine_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q

Tactic:
simp only [← cancel_epi h₂.p, h₂.p_descQ_assoc, assoc, p_opcyclesMap',
  IsIso.inv_hom_id_assoc, comp_id]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem mod_zero (n : Num) : n % 0 = n :=
  show n.mod 0 = n by
    cases n
    · rfl
    · simp [Num.mod]

Proof state:
case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝

Tactic:
simp [Num.mod]

Result:
no goals

Proof state:
case zero

⊢ zero.mod 0 = zero

Tactic:
rfl

Result:
no goals

Proof state:
n : Num
⊢ n.mod 0 = n

Tactic:
cases n

Result:
case zero

⊢ zero.mod 0 = zero

case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mapQ_id (h : p ≤ p.comap LinearMap.id := (by rw [comap_id])) :
    p.mapQ p LinearMap.id h = LinearMap.id

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : optParam (p ≤ comap LinearMap.id p) ⋯
x✝ : M
⊢ (p.mapQ p LinearMap.id h ∘ₗ p.mkQ) x✝ = (LinearMap.id ∘ₗ p.mkQ) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p

Tactic:
rw [comap_id]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : optParam (p ≤ comap LinearMap.id p) ⋯
⊢ p.mapQ p LinearMap.id h = LinearMap.id

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : optParam (p ≤ comap LinearMap.id p) ⋯
x✝ : M
⊢ (p.mapQ p LinearMap.id h ∘ₗ p.mkQ) x✝ = (LinearMap.id ∘ₗ p.mkQ) x✝
-- Mathlib/Combinatorics/Hall/Basic.lean
theorem hallMatchingsOn.nonempty {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α)
    (h : ∀ s : Finset ι, #s ≤ #(s.biUnion t)) (ι' : Finset ι) :
    Nonempty (hallMatchingsOn t ι')

Proof state:
case h.e'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #s' = #(image Subtype.val s')

Tactic:
simp only [card_image_of_injective s' Subtype.coe_injective]

Result:
no goals

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ ∃ x, x ∈ hallMatchingsOn t ι'

Tactic:
apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp

Result:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ ∀ (s : Finset { x // x ∈ ι' }), #s ≤ #(s.biUnion fun i => t ↑i)

Proof state:
case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #(s'.biUnion fun i => t ↑i) = #((image Subtype.val s').biUnion t)

Tactic:
rw [image_biUnion]

Result:
no goals

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #s' ≤ #(s'.biUnion fun i => t ↑i)

Tactic:
convert h (s'.image (↑)) using 1

Result:
case h.e'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #s' = #(image Subtype.val s')

case h.e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #(s'.biUnion fun i => t ↑i) = #((image Subtype.val s').biUnion t)

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ ∀ (s : Finset { x // x ∈ ι' }), #s ≤ #(s.biUnion fun i => t ↑i)

Tactic:
intro s'

Result:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset { x // x ∈ ι' }
⊢ #s' ≤ #(s'.biUnion fun i => t ↑i)

Proof state:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ Nonempty ↑(hallMatchingsOn t ι')

Tactic:
refine ⟨Classical.indefiniteDescription _ ?_⟩

Result:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
⊢ ∃ x, x ∈ hallMatchingsOn t ι'
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem sqLe_add_mixed {c d x y z w : ℕ} (xy : SqLe x c y d) (zw : SqLe z c w d) :
    c * (x * z) ≤ d * (y * w) :=
  Nat.mul_self_le_mul_self_iff.1 <| by
    simpa [mul_comm, mul_left_comm] using mul_le_mul xy zw (Nat.zero_le _) (Nat.zero_le _)

Proof state:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))

Tactic:
simpa [mul_comm, mul_left_comm] using mul_le_mul xy zw (Nat.zero_le _) (Nat.zero_le _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : List α) (init : β) :
    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
l : List α
init : β
⊢ foldl f init (filter p l) = foldl (fun x y => if p y = true then f x y else x) init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filter_cons, foldl_cons]
  split <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
a : α
l : List α
ih : ∀ (init : β), foldl f init (filter p l) = foldl (fun x y => if p y = true then f x y else x) init l
init : β
⊢ foldl f init (filter p (a :: l)) = foldl (fun x y => if p y = true then f x y else x) init (a :: l)

Tactic:
simp only [filter_cons, foldl_cons]

Result:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
a : α
l : List α
ih : ∀ (init : β), foldl f init (filter p l) = foldl (fun x y => if p y = true then f x y else x) init l
init : β
⊢ foldl f init (if p a = true then a :: filter p l else filter p l) =
    foldl (fun x y => if p y = true then f x y else x) (if p a = true then f init a else init) l

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
init : β
⊢ foldl f init (filter p []) = foldl (fun x y => if p y = true then f x y else x) init []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
a : α
l : List α
ih : ∀ (init : β), foldl f init (filter p l) = foldl (fun x y => if p y = true then f x y else x) init l
init : β
⊢ foldl f init (if p a = true then a :: filter p l else filter p l) =
    foldl (fun x y => if p y = true then f x y else x) (if p a = true then f init a else init) l

Tactic:
split <;> simp [ih]

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
The integrand in the definition of `I` is bounded by 1 and the interval has length 2, so the
integral is bounded above by `2`.
-/
private lemma I_le (n : ℕ) : I n (π / 2) ≤ 2

Proof state:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - x ^ 2 ∧ 1 - x ^ 2 ≤ 1

Tactic:
constructor <;> nlinarith

Result:
no goals

Proof state:
n : ℕ
⊢ 1 * |1 - -1| ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ≤ 1

Tactic:
rw [abs_le]

Result:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - x ^ 2 ∧ 1 - x ^ 2 ≤ 1

Proof state:
n : ℕ
⊢ ‖I n (π / 2)‖ ≤ 2

Tactic:
refine (norm_integral_le_of_norm_le_const ?_).trans (show (1 : ℝ) * _ ≤ _ by norm_num)

Result:
n : ℕ
⊢ ∀ x ∈ Ι (-1) 1, ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Proof state:
n : ℕ
⊢ ∀ x ∈ Ι (-1) 1, ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
intros x hx

Result:
n : ℕ
x : ℝ
hx : x ∈ Ι (-1) 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Proof state:
n : ℕ
⊢ I n (π / 2) ≤ 2

Tactic:
rw [← norm_of_nonneg I_pos.le]

Result:
n : ℕ
⊢ ‖I n (π / 2)‖ ≤ 2

Proof state:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ^ n * |cos (x * (π / 2))| ≤ 1

Tactic:
refine mul_le_one₀ (pow_le_one₀ (abs_nonneg _) ?_) (abs_nonneg _) (abs_cos_le_one _)

Result:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ≤ 1

Proof state:
n : ℕ
x : ℝ
hx : x ∈ Ι (-1) 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
simp only [uIoc_of_le, neg_le_self_iff, zero_le_one, mem_Ioc] at hx

Result:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Proof state:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
rw [norm_eq_abs, abs_mul, abs_pow]

Result:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ^ n * |cos (x * (π / 2))| ≤ 1
-- Mathlib/GroupTheory/CoprodI.lean
theorem mem_equivPair_tail_iff {i j : ι} {w : Word M} (m : M i) :
    (⟨i, m⟩ ∈ (equivPair j w).tail.toList) ↔ ⟨i, m⟩ ∈ w.toList.tail
      ∨ i ≠ j ∧ ∃ h : w.toList ≠ [], w.toList.head h = ⟨i, m⟩

Proof state:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
h : ¬j = k
m : M k
ih :
  ⟨k, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x =>
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨k, m⟩ ∈ tail.toList.tail ∨ ¬k = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨k, m⟩
⊢ ⟨k, m⟩ ∈ (↑⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨k, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬k = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨k, m⟩

Tactic:
simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp]
lemma fst_prod [IsProbabilityMeasure ν] : (μ.prod ν).fst = μ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
⊢ (μ.prod ν).fst = μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ.prod ν).fst s = μ s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ.prod ν).fst s = μ s

Tactic:
rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_self_sub_right {m n : ℕ} (h : m ≤ n) : Coprime n (n - m) ↔ Coprime n m

Proof state:
m n : ℕ
h : m ≤ n
⊢ n.Coprime (n - m) ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_self_sub_right h]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem isMultiplicative_zeta : IsMultiplicative ζ :=
  IsMultiplicative.iff_ne_zero.2 ⟨by simp, by simp +contextual⟩

Proof state:
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → ζ (m * n) = ζ m * ζ n

Tactic:
simp +contextual

Result:
no goals

Proof state:
⊢ ζ 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nat_add [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (n : ℕ) (x : G) : f (↑n + x) = f x + n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddCommMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℕ
x : G
⊢ f (↑n + x) = f x + ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
For any real `a`, we have that `a ^ (2n+1) / n!` tends to `0` as `n → ∞`.  This is just a
reformulation of tendsto_pow_div_factorial_atTop, which asserts the same for `a ^ n / n!`
-/
private lemma tendsto_pow_div_factorial_at_top_aux (a : ℝ) :
    Tendsto (fun n => (a : ℝ) ^ (2 * n + 1) / n !) atTop (nhds 0)

Proof state:
a : ℝ
x : ℕ
⊢ a * ((a ^ 2) ^ x / ↑x !) = a ^ (2 * x + 1) / ↑x !

Tactic:
rw [← pow_mul, mul_div_assoc', _root_.pow_succ']

Result:
no goals

Proof state:
a : ℝ
⊢ Tendsto (fun n => a ^ (2 * n + 1) / ↑n !) atTop (nhds (a * 0))

Tactic:
refine ((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)

Result:
a : ℝ
x : ℕ
⊢ a * ((a ^ 2) ^ x / ↑x !) = a ^ (2 * x + 1) / ↑x !

Proof state:
a : ℝ
⊢ Tendsto (fun n => a ^ (2 * n + 1) / ↑n !) atTop (nhds 0)

Tactic:
rw [← mul_zero a]

Result:
a : ℝ
⊢ Tendsto (fun n => a ^ (2 * n + 1) / ↑n !) atTop (nhds (a * 0))