harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Vector α n) :
    l.foldl f b = l.foldlM (m := Id) f b

Proof state:
case mk
β : Type u_1
α : Type u_2
f : β → α → β
b : β
l : Array α
⊢ foldl f b { toArray := l, size_toArray := ⋯ } = foldlM f b { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldl_eq_foldlM]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : β → α → β
b : β
l : Vector α n
⊢ foldl f b l = foldlM f b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
α : Type u_2
f : β → α → β
b : β
l : Array α
⊢ foldl f b { toArray := l, size_toArray := ⋯ } = foldlM f b { toArray := l, size_toArray := ⋯ }
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem finite_of_toPiLocalization_pi_surjective
    (h : Function.Surjective (toPiLocalization (Π i, R i))) :
    Finite ι

Proof state:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Finite ι

Tactic:
contrapose h

Result:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : ¬Finite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))

Proof state:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Infinite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))

Tactic:
exact toPiLocalization_not_surjective_of_infinite _

Result:
no goals

Proof state:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : ¬Finite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))

Tactic:
rw [not_finite_iff_infinite] at h

Result:
ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Infinite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem rootSet_prod [CommRing S] [IsDomain S] [Algebra R S] {ι : Type*} (f : ι → R[X])
    (s : Finset ι) (h : s.prod f ≠ 0) : (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Tactic:
classical
simp only [rootSet, aroots, ← Finset.mem_coe]
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Tactic:
simp only [rootSet, aroots, ← Finset.mem_coe]

Result:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ↑(map (algebraMap R S) (s.prod f)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ↑(map (algebraMap R S) (s.prod f)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

Tactic:
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]

Result:
case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ∏ i ∈ s, map (algebraMap R S) (f i) ≠ 0

Proof state:
case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ∏ i ∈ s, map (algebraMap R S) (f i) ≠ 0

Tactic:
rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNClique_zero : G.IsNClique 0 s ↔ s = ∅

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 0 s ↔ s = ∅

Tactic:
simp only [isNClique_iff, Finset.card_eq_zero, and_iff_right_iff_imp]

Result:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s

Tactic:
rintro rfl

Result:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_nat_pow_near (hx : 1 ≤ x) (hy : 1 < y) : ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1)

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
exact
let n := Nat.find h
have hn : x < y ^ n := Nat.find_spec h
have hnp : 0 < n :=
pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False

Tactic:
rw [hn0, pow_zero] at hn

Result:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy

Result:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
classical exact
    let n := Nat.find h
    have hn : x < y ^ n := Nat.find_spec h
    have hnp : 0 < n :=
      pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
    have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
    have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
    ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False

Tactic:
exact not_le_of_gt hn hx

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemiring α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : n.pred + 1 = n
hltn : n.pred < n
⊢ x < y ^ (n.pred + 1)

Tactic:
rwa [hnsp]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
    IsConj σ τ ↔ #σ.support = #τ.support where
  mp h

Proof state:
case intro.refine_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
x✝ : α
ha : x✝ ∈ σ.support
⊢ (fun a x => π a) x✝ ha ∈ (π * σ * π⁻¹).support

Tactic:
simp [mem_support.1 ha]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : π⁻¹ b ∉ σ.support
⊢ b ∉ (π * σ * π⁻¹).support

Tactic:
rw [mem_support, Classical.not_not] at hb

Result:
case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : σ (π⁻¹ b) = π⁻¹ b
⊢ b ∉ (π * σ * π⁻¹).support

Proof state:
case intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
⊢ #σ.support = #(π * σ * π⁻¹).support

Tactic:
refine Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab)
    fun b hb ↦ ⟨π⁻¹ b, ?_, π.apply_inv_self b⟩

Result:
case intro.refine_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
x✝ : α
ha : x✝ ∈ σ.support
⊢ (fun a x => π a) x✝ ha ∈ (π * σ * π⁻¹).support

case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ (π * σ * π⁻¹).support
⊢ π⁻¹ b ∈ σ.support

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : IsConj σ τ
⊢ #σ.support = #τ.support

Tactic:
obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h

Result:
case intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
⊢ #σ.support = #(π * σ * π⁻¹).support

Proof state:
case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : σ (π⁻¹ b) = π⁻¹ b
⊢ b ∉ (π * σ * π⁻¹).support

Tactic:
rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ (π * σ * π⁻¹).support
⊢ π⁻¹ b ∈ σ.support

Tactic:
contrapose! hb

Result:
case intro.refine_2
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : π⁻¹ b ∉ σ.support
⊢ b ∉ (π * σ * π⁻¹).support
-- Mathlib/CategoryTheory/MorphismProperty/Retract.lean
@[simp]
lemma retracts_le_iff {P Q : MorphismProperty C} [Q.IsStableUnderRetracts] :
    P.retracts ≤ Q ↔ P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ P.retracts ≤ Q

Tactic:
exact le_trans (retracts_monotone h) Q.retracts_le

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P ≤ Q → P.retracts ≤ Q

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ P.retracts ≤ Q

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q ↔ P ≤ Q

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P ≤ Q → P.retracts ≤ Q

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_retracts

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Continuous.lean
theorem Continuous.inner (hf : Continuous f) (hg : Continuous g) : Continuous fun t => ⟪f t, g t⟫ :=
  continuous_iff_continuousAt.2 fun _x => by fun_prop

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : Type u_4
inst✝ : TopologicalSpace α
f g : α → E
hf : Continuous f
hg : Continuous g
_x : α
⊢ ContinuousAt (fun t => Inner.inner (f t) (g t)) _x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.isMax (h : IsSuccPrelimit (succ a)) : IsMax a

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False

Tactic:
exact h a (covBy_succ_of_not_isMax H)

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
⊢ IsMax a

Tactic:
by_contra H

Result:
α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False
-- Mathlib/Analysis/Convex/Extrema.lean
theorem IsMinOn.of_isLocalMinOn_of_convexOn_Icc {f : ℝ → β} {a b : ℝ} (a_lt_b : a < b)
    (h_local_min : IsLocalMinOn f (Icc a b) a) (h_conv : ConvexOn ℝ (Icc a b) f) :
    IsMinOn f (Icc a b) a

Proof state:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ c ∈ {x | (fun x => f a ≤ f x) x}

Tactic:
dsimp only [mem_setOf_eq]

Result:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_neg_of_pos {a : Int} (h : 0 < a) : -a < 0

Proof state:
a : Int
h : 0 < a
⊢ -a < 0

Tactic:
have : -a < -0 := Int.neg_lt_neg h

Result:
a : Int
h : 0 < a
this : -a < -0
⊢ -a < 0

Proof state:
a : Int
h : 0 < a
this : -a < -0
⊢ -a < 0

Tactic:
rwa [Int.neg_zero] at this

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
lemma injective_eq_monomorphisms_iff :
    MorphismProperty.injective C = monomorphisms C ↔ (forget C).PreservesMonomorphisms

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
⊢ monomorphisms C ≤ MorphismProperty.injective C

Tactic:
intro _ _ f hf

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ MorphismProperty.injective C f
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem zero_rpow_of_neg {y : ℝ} (h : y < 0) : (0 : ℝ≥0∞) ^ y = ⊤

Proof state:
y : ℝ
h : y < 0
⊢ (if 0 = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow 0 y)) = ⊤

Tactic:
simp [h, ne_of_gt h]

Result:
no goals

Proof state:
y : ℝ
h : y < 0
⊢ 0 ^ y = ⊤

Tactic:
rw [← ENNReal.coe_zero, ← ENNReal.some_eq_coe]

Result:
y : ℝ
h : y < 0
⊢ some 0 ^ y = ⊤
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_mono {K₀ : PositiveCompacts G} {K₁ K₂ : Compacts G} (h : (K₁ : Set G) ⊆ K₂) :
    chaar K₀ K₁ ≤ chaar K₀ K₂

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0

Tactic:
rw [IsClosed.closure_subset_iff]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
⊢ chaar K₀ K₁ ≤ chaar K₀ K₂

Tactic:
let eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁
⊢ chaar K₀ K₁ ≤ chaar K₀ K₂
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_zero : sin 0 = 0

Proof state:
⊢ sin 0 = 0

Tactic:
simp [sin]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean
@[to_additive]
lemma prod_preimage' (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : Finset κ) (hf) (g : κ → β) :
    ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s with x ∈ Set.range f, g x

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∀ x ∈ s.preimage f hf, ∀ y ∈ s.preimage f hf, f x = f y → x = y

Tactic:
simpa only [mem_preimage, Set.InjOn] using hf

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∏ x ∈ image f (s.preimage f hf), g x = ∏ x ∈ filter (fun x => x ∈ Set.range f) s, g x

Tactic:
rw [image_preimage]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ filter (fun x => x ∈ Set.range f) s, g x

Tactic:
calc
  ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
    Eq.symm <| prod_image <| by simpa only [mem_preimage, Set.InjOn] using hf
  _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst✝¹ : CommMonoid β
f : ι → κ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' ↑s)
g : κ → β
⊢ ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ filter (fun x => x ∈ Set.range f) s, g x

Tactic:
classical
calc
  ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
    Eq.symm <| prod_image <| by simpa only [mem_preimage, Set.InjOn] using hf
  _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem toTopologicalSpace_injective :
    Function.Injective (toTopologicalSpace : GroupTopology α → TopologicalSpace α) :=
  fun f g h => by
    cases f
    cases g
    congr

Proof state:
α : Type u
inst✝ : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Tactic:
cases f

Result:
case mk
α : Type u
inst✝ : Group α
g : GroupTopology α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalGroup✝ : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ } = g

Proof state:
case mk
α : Type u
inst✝ : Group α
g : GroupTopology α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalGroup✝ : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ } = g

Tactic:
cases g

Result:
case mk.mk
α : Type u
inst✝ : Group α
toTopologicalSpace✝¹ : TopologicalSpace α
toIsTopologicalGroup✝¹ : IsTopologicalGroup α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalGroup✝ : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalGroup := toIsTopologicalGroup✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalGroup := toIsTopologicalGroup✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }

Proof state:
case mk.mk
α : Type u
inst✝ : Group α
toTopologicalSpace✝¹ : TopologicalSpace α
toIsTopologicalGroup✝¹ : IsTopologicalGroup α
toTopologicalSpace✝ : TopologicalSpace α
toIsTopologicalGroup✝ : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalGroup := toIsTopologicalGroup✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalGroup := toIsTopologicalGroup✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalGroup := toIsTopologicalGroup✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Iic : (fun x => x - a) ⁻¹' Iic b = Iic (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) ⁻¹' Iic b = Iic (b + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- To prove `FermatLastTheoremFor 3`, it is enough to prove `FermatLastTheoremForThreeGen`. -/
lemma FermatLastTheoremForThree_of_FermatLastTheoremThreeGen
    [NumberField K] [IsCyclotomicExtension {3} ℚ K] :
    FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3

Proof state:
case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ↑a ↑b

Tactic:
rw [show a = algebraMap _ (𝓞 K) a by simp, show b = algebraMap _ (𝓞 K) b by simp]

Result:
case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ((algebraMap ℤ (𝓞 K)) a) ((algebraMap ℤ (𝓞 K)) b)

Proof state:
case refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : λ ∣ ↑a
⊢ 3 ∣ a

Tactic:
rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
  hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ ↑c ≠ 0

Tactic:
simp [hc]

Result:
no goals

Proof state:
case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ((algebraMap ℤ (𝓞 K)) a) ((algebraMap ℤ (𝓞 K)) b)

Tactic:
exact hcoprime.map _

Result:
no goals