harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructions.lean
theorem exists_finset_piecewise_mem_of_mem_nhds [DecidableEq ι] {s : Set (∀ a, π a)} {x : ∀ a, π a}
    (hs : s ∈ 𝓝 x) (y : ∀ a, π a) : ∃ I : Finset ι, I.piecewise x y ∈ s

Proof state:
case intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
refine ⟨I, hts fun i hi => ?_⟩

Result:
case intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ I.piecewise x y i ∈ t i

Proof state:
case intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ I.piecewise x y i ∈ t i

Tactic:
simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
rcases hs with ⟨I, t, htx, hts⟩

Result:
case intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x : (a : ι) → π a
hs : s ∈ 𝓝 x
y : (a : ι) → π a
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
simp only [nhds_pi, Filter.mem_pi'] at hs

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem mass_zero_iff (μ : FiniteMeasure Ω) : μ.mass = 0 ↔ μ = 0

Proof state:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ ↑μ univ = 0

Tactic:
rwa [← ennreal_mass, ENNReal.coe_eq_zero]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
hμ : μ = 0
⊢ μ.mass = 0

Tactic:
simp only [hμ, zero_mass]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.mass = 0 ↔ μ = 0

Tactic:
refine ⟨fun μ_mass => ?_, fun hμ => by simp only [hμ, zero_mass]⟩

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ μ = 0

Proof state:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ ↑μ = ↑0

Tactic:
apply Measure.measure_univ_eq_zero.mp

Result:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ ↑μ univ = 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ μ = 0

Tactic:
apply toMeasure_injective

Result:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ ↑μ = ↑0
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem mem_support_iff_exists_append {V : Type u} {G : SimpleGraph V} {u v w : V}
    {p : G.Walk u v} : w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ ∃ q r, p = q.append r

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ q r, p = q.append r

case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ q r, p = q.append r

Tactic:
exact fun h => ⟨_, _, (p.take_spec h).symm⟩

Result:
no goals

Proof state:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk u w
r : G.Walk w v
⊢ w ∈ (q.append r).support

Tactic:
simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support

Tactic:
rintro ⟨q, r, rfl⟩

Result:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk u w
r : G.Walk w v
⊢ w ∈ (q.append r).support
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_two (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun z => id z * id z) a = a * a

Tactic:
rw [cfcₙ_mul id id a, cfcₙ_id ℝ≥0 a]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 2 = a * a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_two]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x * x) a = a * a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x * x) a = a * a

Tactic:
change cfcₙ (fun z : ℝ≥0 => id z * id z) a = a * a

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun z => id z * id z) a = a * a
-- Mathlib/Algebra/Order/Sub/Defs.lean
/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add_rev` assuming that `a = b + c` itself is
cancellable rather than `b`. -/
protected lemma tsub_eq_of_eq_add_rev' [AddLeftMono α]
    (ha : AddLECancellable a) (h : a = b + c) : a - b = c :=
  ha.tsub_eq_of_eq_add' <| by rw [add_comm, h]

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
ha : AddLECancellable a
h : a = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem transpose_eq_iff_eq_transpose {μ ν : YoungDiagram} : μ.transpose = ν ↔ μ = ν.transpose

Proof state:
case mpr
ν : YoungDiagram
⊢ ν.transpose.transpose = ν

Tactic:
simp

Result:
no goals

Proof state:
case mpr
μ ν : YoungDiagram
⊢ μ = ν.transpose → μ.transpose = ν

Tactic:
rintro rfl

Result:
case mpr
ν : YoungDiagram
⊢ ν.transpose.transpose = ν
-- Mathlib/Logic/Function/Basic.lean
theorem injective_comp_right_iff_surjective {γ : Type*} [Nontrivial γ] :
    Injective (fun g : β → γ ↦ g ∘ f) ↔ Surjective f

Proof state:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g => g ∘ f) fun x => c) = (fun g => g ∘ f) fun x => if x = b₀ then c' else c

Tactic:
ext a

Result:
case refine_1.h
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
a : α
⊢ (fun g => g ∘ f) (fun x => c) a = (fun g => g ∘ f) (fun x => if x = b₀ then c' else c) a

Proof state:
case refine_1.h
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
a : α
⊢ (fun g => g ∘ f) (fun x => c) a = (fun g => g ∘ f) (fun x => if x = b₀ then c' else c) a

Tactic:
simp only [comp_apply, if_neg fun h ↦ hb ⟨a, h⟩]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
⊢ c = c'

Tactic:
have ⟨b₀, hb⟩ := not_forall.mp not_surj

Result:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ c = c'

Proof state:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g => g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x => c) = fun x => if x = b₀ then c' else c
⊢ c = c'

Tactic:
simpa using congr_fun this b₀

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem not_exists_int_prime_dvd_sub_of_prime_ne_two
    [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
    ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : p ^ (k + 1) = 2
⊢ ↑p ^ (k + 1) = 2

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : p ^ (k + 1) = 2
⊢ False

Tactic:
simp_all only [(@Nat.Prime.pow_eq_iff 2 p (k+1) Nat.prime_two).mp (by assumption_mod_cast),
  pow_one, ne_eq]

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
⊢ ¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n

Tactic:
refine not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun h ↦ ?_)

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : p ^ (k + 1) = 2
⊢ False
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Proof state:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Tactic:
exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial
-- Mathlib/Order/ModularLattice.lean
lemma Set.Iic.isCompl_inf_inf_of_isCompl_of_le [Lattice α] [BoundedOrder α] [IsModularLattice α]
    {a b c : α} (h₁ : IsCompl b c) (h₂ : b ≤ a) :
    IsCompl (⟨a ⊓ b, inf_le_left⟩ : Iic a) (⟨a ⊓ c, inf_le_left⟩ : Iic a)

Proof state:
case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ (b ⊓ a ⊔ c) ⊓ a = a

Tactic:
simp [inf_of_le_left h₂, h₁.sup_eq_top]

Result:
no goals

Proof state:
case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Codisjoint ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Tactic:
simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]

Result:
case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ (b ⊓ a ⊔ c) ⊓ a = a

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ IsCompl ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Tactic:
constructor

Result:
case disjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Disjoint ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Codisjoint ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Proof state:
case disjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Disjoint ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Tactic:
simp [disjoint_iff, Subtype.ext_iff, inf_comm a c, inf_assoc a, ← inf_assoc b, h₁.inf_eq_bot]

Result:
no goals
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Proof state:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34

Tactic:
simp_rw [sum_range_succ]

Result:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |∑ x ∈ range 0, 2⁻¹ ^ (x + 1) / (↑x + 1) + 2⁻¹ ^ (0 + 1) / (↑0 + 1) + 2⁻¹ ^ (1 + 1) / (↑1 + 1) +
                                                                        2⁻¹ ^ (2 + 1) / (↑2 + 1) +
                                                                      2⁻¹ ^ (3 + 1) / (↑3 + 1) +
                                                                    2⁻¹ ^ (4 + 1) / (↑4 + 1) +
                                                                  2⁻¹ ^ (5 + 1) / (↑5 + 1) +
                                                                2⁻¹ ^ (6 + 1) / (↑6 + 1) +
                                                              2⁻¹ ^ (7 + 1) / (↑7 + 1) +
                                                            2⁻¹ ^ (8 + 1) / (↑8 + 1) +
                                                          2⁻¹ ^ (9 + 1) / (↑9 + 1) +
                                                        2⁻¹ ^ (10 + 1) / (↑10 + 1) +
                                                      2⁻¹ ^ (11 + 1) / (↑11 + 1) +
                                                    2⁻¹ ^ (12 + 1) / (↑12 + 1) +
                                                  2⁻¹ ^ (13 + 1) / (↑13 + 1) +
                                                2⁻¹ ^ (14 + 1) / (↑14 + 1) +
                                              2⁻¹ ^ (15 + 1) / (↑15 + 1) +
                                            2⁻¹ ^ (16 + 1) / (↑16 + 1) +
                                          2⁻¹ ^ (17 + 1) / (↑17 + 1) +
                                        2⁻¹ ^ (18 + 1) / (↑18 + 1) +
                                      2⁻¹ ^ (19 + 1) / (↑19 + 1) +
                                    2⁻¹ ^ (20 + 1) / (↑20 + 1) +
                                  2⁻¹ ^ (21 + 1) / (↑21 + 1) +
                                2⁻¹ ^ (22 + 1) / (↑22 + 1) +
                              2⁻¹ ^ (23 + 1) / (↑23 + 1) +
                            2⁻¹ ^ (24 + 1) / (↑24 + 1) +
                          2⁻¹ ^ (25 + 1) / (↑25 + 1) +
                        2⁻¹ ^ (26 + 1) / (↑26 + 1) +
                      2⁻¹ ^ (27 + 1) / (↑27 + 1) +
                    2⁻¹ ^ (28 + 1) / (↑28 + 1) +
                  2⁻¹ ^ (29 + 1) / (↑29 + 1) +
                2⁻¹ ^ (30 + 1) / (↑30 + 1) +
              2⁻¹ ^ (31 + 1) / (↑31 + 1) +
            2⁻¹ ^ (32 + 1) / (↑32 + 1) +
          2⁻¹ ^ (33 + 1) / (↑33 + 1) -
        287209 / 414355| ≤
    1 / 10 ^ 10 - 1 / 2 ^ 34
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The evaluation map on automorphisms is injective for connected objects. -/
lemma evaluation_aut_injective_of_isConnected (A : C) [IsConnected A] (a : F.obj A) :
    Function.Injective (fun f : Aut A ↦ F.map (f.hom) a)

Proof state:
case hg
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => F.map f a

Tactic:
exact evaluation_injective_of_isConnected F A A a

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => F.map f.hom a

Tactic:
show Function.Injective ((fun f : A ⟶ A ↦ F.map f a) ∘ (fun f : Aut A ↦ f.hom))

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective ((fun f => F.map f a) ∘ fun f => f.hom)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective ((fun f => F.map f a) ∘ fun f => f.hom)

Tactic:
apply Function.Injective.comp

Result:
case hg
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => F.map f a

case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => f.hom

Proof state:
case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective fun f => f.hom

Tactic:
exact @Aut.ext _ _ A

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.dual_iff {t : Ordnode α} : Sized (.dual t) ↔ Sized t :=
  ⟨fun h => by rw [← dual_dual t]; exact h.dual, Sized.dual⟩

Proof state:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.Sized

Tactic:
rw [← dual_dual t]

Result:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Proof state:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Tactic:
exact h.dual

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_blockDiagonal' [DecidableEq α] (d : ∀ i : α, Matrix (m' i) (m' i) R) :
    BlockTriangular (blockDiagonal' d) Sigma.fst

Proof state:
case mk.mk
α : Type u_1
m' : α → Type u_6
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0

Tactic:
apply blockDiagonal'_apply_ne d i' j' fun h' => ne_of_lt h h'.symm

Result:
no goals

Proof state:
α : Type u_1
m' : α → Type u_6
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ (blockDiagonal' d).BlockTriangular Sigma.fst

Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h

Result:
case mk.mk
α : Type u_1
m' : α → Type u_6
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measurable_of_Iic {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iic x)) : Measurable f

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ Measurable f

Tactic:
apply measurable_of_Ioi

Result:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)

Proof state:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)

Tactic:
simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]

Result:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)

Proof state:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)

Tactic:
assumption

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_range_left {f : G ⧸ H → G} (hf : ∀ q, ↑(f q) = q) :
    IsComplement (range f) H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ IsComplement (range f) ↑H

Tactic:
rw [isComplement_subgroup_right_iff_bijective]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Bijective ((range f).restrict QuotientGroup.mk)

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h : (range f).restrict QuotientGroup.mk ⟨f q₁, ⋯⟩ = (range f).restrict QuotientGroup.mk ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Tactic:
exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Bijective ((range f).restrict QuotientGroup.mk)

Tactic:
refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Injective ((range f).restrict QuotientGroup.mk)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Injective ((range f).restrict QuotientGroup.mk)

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h : (range f).restrict QuotientGroup.mk ⟨f q₁, ⋯⟩ = (range f).restrict QuotientGroup.mk ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩