harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
lemma range_weylGroupToPerm :
    P.weylGroupToPerm.range = Subgroup.closure (range P.reflection_perm)

Proof state:
case refine_2.intro.mk.mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ P.reflection_perm i ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)

Result:
no goals

Proof state:
case refine_1.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ P.reflection_perm i ∈ ↑P.weylGroupToPerm.range

Tactic:
simp only [MonoidHom.restrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
  SetLike.mem_coe]

Result:
case refine_1.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ ∃ x ∈ P.weylGroup, (Equiv.indexHom P) x = P.reflection_perm i

Proof state:
case refine_2.intro.mk.inv_mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ P.weylGroupToPerm ⟨(Equiv.reflection P i)⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.indexHom_apply,
  Equiv.reflection_indexEquiv]

Result:
case refine_2.intro.mk.inv_mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ P.reflection_perm i ∈ Subgroup.closure (range P.reflection_perm)

Proof state:
case refine_2.intro.mk.mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ P.weylGroupToPerm ⟨Equiv.reflection P i, ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
simp only [MonoidHom.restrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]

Result:
case refine_2.intro.mk.mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ P.reflection_perm i ∈ Subgroup.closure (range P.reflection_perm)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (Equiv.indexHom P) (Equiv.reflection P i) = P.reflection_perm i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem of_mulHom_image [DecidableEq H] (f : G →ₙ* H)
    (hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d)
    (h : UniqueMul (A.image f) (B.image f) (f a0) (f b0)) : UniqueMul A B a0 b0 :=
  fun a b ha hb ab ↦ hf ab
    (h (Finset.mem_image_of_mem f ha) (Finset.mem_image_of_mem f hb) <| by simp_rw [← map_mul, ab])

Proof state:
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ f a * f b = f a0 * f b0

Tactic:
simp_rw [← map_mul, ab]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem Antitone.ne_of_lt_of_lt_nat {f : ℕ → α} (hf : Antitone f) (n : ℕ) {x : α}
    (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℕ) : f a ≠ x

Proof state:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h1)

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl

Result:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup_product_left (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f ⟨i, i'⟩ :=
  eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
a : α
⊢ (s ×ˢ t).sup f ≤ a ↔ (s.sup fun i => t.sup fun i' => f (i, i')) ≤ a

Tactic:
simp [@forall_swap _ γ]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_def (G : C) :
    IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g :=
  ⟨fun hG X Y f g hfg =>
    hG _ _ fun H hH h => by
      obtain rfl := Set.mem_singleton_iff.1 hH
      exact hfg h,
    fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (Set.mem_singleton _) _⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
H : C
h : Y ⟶ H
hG : IsCoseparator H
hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h
hH : H ∈ {H}
⊢ f ≫ h = g ≫ h

Tactic:
exact hfg h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : H ∈ {G}
h : Y ⟶ H
⊢ f ≫ h = g ≫ h

Tactic:
obtain rfl := Set.mem_singleton_iff.1 hH

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
H : C
h : Y ⟶ H
hG : IsCoseparator H
hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h
hH : H ∈ {H}
⊢ f ≫ h = g ≫ h
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem Tendsto.eventually_forall_le_atBot [Preorder β] {l : Filter α}
    {p : β → Prop} {f : α → β} (hf : Tendsto f l atBot) (h_evtl : ∀ᶠ x in atBot, p x) :
    ∀ᶠ x in l, ∀ y, y ≤ f x → p y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
rw [← Filter.eventually_forall_le_atBot] at h_evtl

Result:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
exact (h_evtl.comap f).filter_mono hf.le_comap

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_lt_mul_of_pos_left {a b c : Int}
  (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * (b - a)
⊢ c * a < c * b

Tactic:
rw [Int.mul_sub] at this

Result:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * b - c * a
⊢ c * a < c * b

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * b - c * a
⊢ c * a < c * b

Tactic:
exact Int.lt_of_sub_pos this

Result:
no goals

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
⊢ c * a < c * b

Tactic:
have : 0 < c * (b - a) := Int.mul_pos h₂ (Int.sub_pos_of_lt h₁)

Result:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * (b - a)
⊢ c * a < c * b
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
theorem map_id :
    map n (LinearMap.id (R := R) (M := M)) = LinearMap.id

Proof state:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ map n LinearMap.id = LinearMap.id

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_orthonormal' (f : ι → E) :
    Orthonormal 𝕜 fun i : { i | gramSchmidtNormed 𝕜 f i ≠ 0 } => gramSchmidtNormed 𝕜 f i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬↑i = ↑j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0

Tactic:
simp [gramSchmidtNormed, inner_smul_left, inner_smul_right, gramSchmidt_orthogonal 𝕜 f hij]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ Pairwise fun i j => inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0

Tactic:
rintro i j (hij : ¬_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬i = j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ Orthonormal 𝕜 fun i => gramSchmidtNormed 𝕜 f ↑i

Tactic:
refine ⟨fun i => gramSchmidtNormed_unit_length' i.prop, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ Pairwise fun i j => inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬i = j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0

Tactic:
rw [Subtype.ext_iff] at hij

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬↑i = ↑j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem is_localization_basicOpen_of_qcqs {X : Scheme} {U : X.Opens} (hU : IsCompact U.1)
    (hU' : IsQuasiSeparated U.1) (f : Γ(X, U)) :
    IsLocalization.Away f (Γ(X, X.basicOpen f))

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0 → ∃ c, ↑c * z = 0

Tactic:
intro H

Result:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
⊢ ∃ c, ↑c * z = 0

Proof state:
case surj'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

Tactic:
intro z

Result:
case surj'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
z : ↑Γ(X, X.basicOpen f)
⊢ ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
lemma toAut_surjective_isGalois (t : Aut F) (X : C) [IsGalois X]
    [MulAction.IsPretransitive G (F.obj X)] :
    ∃ (g : G), ∀ (x : F.obj X), g • x = t.hom.app X x

Proof state:
case intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).carrier
a : (F.obj X).carrier
⊢ ∃ g, ∀ (x : (F.obj X).carrier), g • x = t.hom.app X x

Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G a (t.hom.app X a)

Result:
case intro.intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).carrier
a : (F.obj X).carrier
g : G
hg : g • a = t.hom.app X a
⊢ ∃ g, ∀ (x : (F.obj X).carrier), g • x = t.hom.app X x

Proof state:
case intro.intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).carrier
a : (F.obj X).carrier
g : G
hg : g • a = t.hom.app X a
⊢ ∃ g, ∀ (x : (F.obj X).carrier), g • x = t.hom.app X x

Tactic:
exact ⟨g, action_ext_of_isGalois F _ hg⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).carrier
⊢ ∃ g, ∀ (x : (F.obj X).carrier), g • x = t.hom.app X x

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F X

Result:
case intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).carrier
a : (F.obj X).carrier
⊢ ∃ g, ∀ (x : (F.obj X).carrier), g • x = t.hom.app X x
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma FermatLastTheoremWith.fermatLastTheoremWith' {α : Type*} [CommSemiring α] {n : ℕ}
    (h : FermatLastTheoremWith α n) : FermatLastTheoremWith' α n :=
  fun a b c _ _ _ _ ↦ by exfalso; apply h a b c <;> assumption

Proof state:
α : Type u_2
inst✝ : CommSemiring α
n : ℕ
h : FermatLastTheoremWith α n
a b c : α
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
apply h a b c <;> assumption

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemiring α
n : ℕ
h : FermatLastTheoremWith α n
a b c : α
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
exfalso

Result:
α : Type u_2
inst✝ : CommSemiring α
n : ℕ
h : FermatLastTheoremWith α n
a b c : α
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ False
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem liminf_preimage_iterate_ae_eq {f : α → α} (hf : QuasiMeasurePreserving f μ μ)
    (hs : f ⁻¹' s =ᵐ[μ] s) : liminf (α := Set α) (fun n => (preimage f)^[n] s) atTop =ᵐ[μ] s :=
  liminf_ae_eq_of_forall_ae_eq (fun n => (preimage f)^[n] s) fun n ↦ by
    simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (fun n => (preimage f)^[n] s) n =ᵐ[μ] s

Tactic:
simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_Prop {p : α → Prop} : Continuous p ↔ IsOpen { x | p x }

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ x ∈ {x | p x}, {x | p x} ∈ 𝓝 x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ Continuous p ↔ IsOpen {x | p x}

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ x ∈ {x | p x}, {x | p x} ∈ 𝓝 x
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem eq_sum_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    map φ P =
      ⟨φ P.a, φ P.a * -(x + y + z), φ P.a * (x * y + x * z + y * z), φ P.a * -(x * y * z)⟩

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }

Tactic:
apply_fun @toPoly _ _

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly =
    { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }.toPoly

case inj
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Function.Injective toPoly

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly =
    { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }.toPoly

Tactic:
rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]

Result:
no goals

Proof state:
case inj
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Function.Injective toPoly

Tactic:
exact fun P Q ↦ (toPoly_injective P Q).mp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜}
    (hf : ∀ i ∈ L, f i =O[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) =O[l] (fun x ↦ (L.map (g · x)).prod)

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
L : List ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ L, f i =O[l] g i
⊢ (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod

Tactic:
induction L with
| nil => simp [isBoundedUnder_const]
| cons i L ihL =>
  simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
  exact hf.1.mul (ihL hf.2)

Result:
no goals

Proof state:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
hf : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
⊢ (fun x => (List.map (fun x_1 => f x_1 x) (i :: L)).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) (i :: L)).prod

Tactic:
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢

Result:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
hf : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod

Proof state:
case nil
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ [], f i =O[l] g i
⊢ (fun x => (List.map (fun x_1 => f x_1 x) []).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) []).prod

Tactic:
simp [isBoundedUnder_const]

Result:
no goals

Proof state:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
hf : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) =O[l] fun x =>
    g i x * (List.map (fun x_1 => g x_1 x) L).prod

Tactic:
exact hf.1.mul (ihL hf.2)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_inv_app_right :
    (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.right = iY.inv

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/Analysis/Fourier/Inversion.lean
theorem MeasureTheory.Integrable.fourier_inversion_inv
    (hf : Integrable f) (h'f : Integrable (𝓕 f)) {v : V}
    (hv : ContinuousAt f v) : 𝓕 (𝓕⁻ f) v = f v

Proof state:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
exact fourier_inversion hf h'f hv

Result:
no goals

Proof state:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
rw [fourierIntegralInv_comm]

Result:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_zero : spanSingleton S (0 : P) = 0

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ x✝ ∈ spanSingleton S 0 ↔ x✝ ∈ 0

Tactic:
simp [Submodule.mem_span_singleton, eq_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ spanSingleton S 0 = 0

Tactic:
ext

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ x✝ ∈ spanSingleton S 0 ↔ x✝ ∈ 0
-- Mathlib/LinearAlgebra/Orientation.lean
theorem Orientation.map_refl : (Orientation.map ι <| LinearEquiv.refl R M) = Equiv.refl _

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)

Tactic:
rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]

Result:
no goals