harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem inv_mul_mem_range_inl : (σ g)⁻¹ * σ' g ∈ S.inl.range

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ (σ g)⁻¹ * σ' g ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
  inv_mul_cancel]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
theorem eulerProduct_hasProd_mulIndicator (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
    HasProd (Set.mulIndicator {p | Nat.Prime p} fun p ↦  ∑' e, f (p ^ e)) (∑' n, f n)

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
⊢ HasProd ((fun p => ∑' (e : ℕ), f (p ^ e)) ∘ Subtype.val) (∑' (n : ℕ), f n)

Tactic:
exact eulerProduct_hasProd hf₁ hmul hsum hf₀

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
⊢ HasProd ({p | Nat.Prime p}.mulIndicator fun p => ∑' (e : ℕ), f (p ^ e)) (∑' (n : ℕ), f n)

Tactic:
rw [← hasProd_subtype_iff_mulIndicator]

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
⊢ HasProd ((fun p => ∑' (e : ℕ), f (p ^ e)) ∘ Subtype.val) (∑' (n : ℕ), f n)
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma mem_stabilizer_mk_iff (φ : K →+* ℂ) (σ : K ≃ₐ[k] K) :
    σ ∈ Stab (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
⊢ φ.comp ↑σ.symm = φ ∨ star φ = φ.comp ↑σ.symm ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm

Tactic:
refine or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
H : φ.comp ↑σ.symm = φ
⊢ σ = 1

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
⊢ φ.comp ↑σ.symm = φ ∨ ComplexEmbedding.conjugate (φ.comp ↑σ.symm) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
rw [← ComplexEmbedding.isConj_symm, ComplexEmbedding.conjugate, star_eq_iff_star_eq]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
⊢ φ.comp ↑σ.symm = φ ∨ star φ = φ.comp ↑σ.symm ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
⊢ σ ∈ Stab (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
simp only [MulAction.mem_stabilizer_iff, smul_mk, mk_eq_iff]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
⊢ φ.comp ↑σ.symm = φ ∨ ComplexEmbedding.conjugate (φ.comp ↑σ.symm) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : K ≃ₐ[k] K
H : φ.comp ↑σ.symm = φ
⊢ σ = 1

Tactic:
exact congr_arg AlgEquiv.symm
  (AlgEquiv.ext (g := AlgEquiv.refl) fun x ↦ φ.injective (RingHom.congr_fun H x))

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem tangentConeAt.lim_zero {α : Type*} (l : Filter α) {c : α → 𝕜} {d : α → E}
    (hc : Tendsto (fun n => ‖c n‖) l atTop) (hd : Tendsto (fun n => c n • d n) l (𝓝 y)) :
    Tendsto d l (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
y : E
α : Type u_5
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto (fun x => ‖d x‖) l (𝓝 0)

Tactic:
exact D

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
y : E
α : Type u_5
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
y : E
α : Type u_5
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto (fun x => ‖d x‖) l (𝓝 0)
-- Mathlib/Data/Nat/Lattice.lean
theorem iSup_le_succ' (u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = u 0 ⊔ ⨆ k ≤ n, u (k + 1)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem card_isConj_eq :
    Nat.card {h : Perm α | IsConj g h} =
      (Fintype.card α)! /
        ((Fintype.card α - g.cycleType.sum)! *
          g.cycleType.prod *
          (∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 < Nat.card ↥(centralizer {g})

Tactic:
apply Nat.card_pos

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← nat_card_centralizer g]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 < Nat.card ↥(centralizer {g})

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} =
    (Fintype.card α)! /
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)

Tactic:
rw [← card_isConj_mul_eq g, Nat.div_eq_of_eq_mul_left _]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_exist (F : X.Presheaf C) (x : X) (t : ToType (stalk.{v, u} F x)) :
    ∃ (U : Opens X) (m : x ∈ U) (s : ToType (F.obj (op U))), F.germ _ x m s = t

Proof state:
case intro.intro.h.mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
        (op { obj := V, property := m })),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          (op { obj := V, property := m }) s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
intro s e

Result:
case intro.intro.h.mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
s :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
    (op { obj := V, property := m })
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
      (op { obj := V, property := m }) s =
    t
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t
-- Mathlib/Algebra/Algebra/Operations.lean
theorem prod_span {ι : Type*} (s : Finset ι) (M : ι → Set A) :
    (∏ i ∈ s, Submodule.span R (M i)) = Submodule.span R (∏ i ∈ s, M i)

Proof state:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)

Tactic:
rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i) → ∏ i ∈ insert a s, span R (M i) = span R (∏ i ∈ insert a s, M i)

Tactic:
intro _ _ H ih

Result:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
ih : ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i)
⊢ ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ ∅, span R (M i) = span R (∏ i ∈ ∅, M i)

case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i) → ∏ i ∈ insert a s, span R (M i) = span R (∏ i ∈ insert a s, M i)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
⊢ ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)

Tactic:
letI := Classical.decEq ι

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i)

Proof state:
case refine_1
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i ∈ ∅, span R (M i) = span R (∏ i ∈ ∅, M i)

Tactic:
simp [one_eq_span, Set.singleton_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map_comp_map {f g h : α → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h]
    (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h a) :
    Sigma.map q ≫ Sigma.map q' = Sigma.map (fun a => q a ≫ q' a)

Proof state:
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a => q a ≫ q' a

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map q' = ι f b✝ ≫ map fun a => q a ≫ q' a

Proof state:
case h
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map q' = ι f b✝ ≫ map fun a => q a ≫ q' a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/MinMax.lean
theorem min_comm (a b : Nat) : min a b = min b a

Proof state:
a b : Nat
h : b < a
⊢ min a b = min b a

Tactic:
simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]

Result:
no goals

Proof state:
a b : Nat
h : a = b
⊢ min a b = min b a

Tactic:
simp [Nat.min_def, h]

Result:
no goals

Proof state:
a b : Nat
⊢ min a b = min b a

Tactic:
match Nat.lt_trichotomy a b with
| .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
| .inr (.inl h) => simp [Nat.min_def, h]
| .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]

Result:
no goals

Proof state:
a b : Nat
h : a < b
⊢ min a b = min b a

Tactic:
simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
theorem isUniformInducing_postcomp
    {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [Module 𝕜 G]
    (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
    IsUniformInducing (g.compContinuousMultilinearMap :
      ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G)

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing g.compContinuousMultilinearMap

Tactic:
rw [← isUniformInducing_toUniformOnFun.of_comp_iff]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing (toUniformOnFun ∘ g.compContinuousMultilinearMap)

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing (toUniformOnFun ∘ g.compContinuousMultilinearMap)

Tactic:
exact (UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem hasStrictFDerivAt_norm_sq (x : F) :
    HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ x)) x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x => re (inner x x)) (2 • (innerSL ℝ) x) x

Tactic:
convert (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)

Result:
case h.e'_12.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 2 • (innerSL ℝ) x =
    (fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))

Proof state:
case h.e'_12.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 2 • (innerSL ℝ) x =
    (fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))

Tactic:
ext y

Result:
case h.e'_12.h.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
y : F
⊢ (2 • (innerSL ℝ) x) y =
    ((fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))) y

Proof state:
case h.e'_12.h.h.h.h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_4✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝¹ : NormedSpace.toModule = NormedSpace.toModule
e_8✝ : instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
y : F
⊢ (2 • (innerSL ℝ) x) y =
    ((fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))) y

Tactic:
simp [two_smul, real_inner_comm]

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x

Tactic:
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x => re (inner x x)) (2 • (innerSL ℝ) x) x
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) :
    e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃

Tactic:
rw [← comp_hom₃, e.inv_hom_id, id_hom₃]

Result:
no goals
-- Mathlib/Computability/Encoding.lean
theorem decode_encodeNat : ∀ n, decodeNat (encodeNat n) = n

Proof state:
⊢ ∀ (n : ℕ), decodeNat (encodeNat n) = n

Tactic:
intro n

Result:
n : ℕ
⊢ decodeNat (encodeNat n) = n

Proof state:
n : ℕ
⊢ decodeNat (encodeNat n) = n

Tactic:
conv_rhs => rw [← Num.to_of_nat n]

Result:
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n

Proof state:
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n

Tactic:
exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)

Result:
no goals
-- Mathlib/Data/Nat/Basic.lean
@[simp] protected lemma pow_eq_one : a ^ n = 1 ↔ a = 1 ∨ n = 0

Proof state:
a n : ℕ
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
a : ℕ
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

case inr
a n : ℕ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Proof state:
case inr
a n : ℕ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
simpa [hn] using Nat.pow_left_inj hn (b := 1)

Result:
no goals

Proof state:
case inl
a : ℕ
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem isComplex_iff {w : InfinitePlace K} :
    IsComplex w ↔ ¬ComplexEmbedding.IsReal (embedding w)

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding

Tactic:
rintro ⟨φ, ⟨hφ, rfl⟩⟩

Result:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Proof state:
case intro.intro.inl
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
rwa [h] at hφ

Result:
no goals

Proof state:
case intro.intro.inr
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding

Proof state:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
contrapose! hφ

Result:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
⊢ ComplexEmbedding.IsReal φ

Proof state:
case intro.intro
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
⊢ ComplexEmbedding.IsReal φ

Tactic:
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
| inl h => rwa [h] at hφ
| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem pos_of_div_pos {a b : Nat} (h : 0 < a / b) : 0 < a

Proof state:
a✝ b : Nat
h : 0 < a✝ / (b + 1)
a : Nat
x✝ : 0 < (a + 1) / (b + 1)
⊢ 0 < a + 1

Tactic:
exact zero_lt_succ a

Result:
no goals

Proof state:
case succ
a b : Nat
h : 0 < a / (b + 1)
⊢ 0 < a

Tactic:
match a, h with
| 0, h => simp at h
| a + 1, _ => exact zero_lt_succ a

Result:
no goals

Proof state:
case zero
a : Nat
h : 0 < a / 0
⊢ 0 < a

Tactic:
simp at h

Result:
no goals

Proof state:
a b : Nat
h✝ : 0 < a / (b + 1)
h : 0 < 0 / (b + 1)
⊢ 0 < 0

Tactic:
simp at h

Result:
no goals

Proof state:
a b : Nat
h : 0 < a / b
⊢ 0 < a

Tactic:
cases b with
| zero => simp at h
| succ b =>
  match a, h with
  | 0, h => simp at h
  | a + 1, _ => exact zero_lt_succ a

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem IsPathConnected.preimage_coe {U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) :
    IsPathConnected (((↑) : U → X) ⁻¹' W)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val ⁻¹' W)

Tactic:
rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]

Result:
no goals