harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem contDiff_norm_sq : ContDiff ℝ n fun x : E => ‖x‖ ^ 2

Proof state:
case h.e'_10.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (⇑reCLM ∘ fun x => inner (id x) (id x)) x✝

Tactic:
exact (inner_self_eq_norm_sq _).symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
⊢ ContDiff ℝ n fun x => ‖x‖ ^ 2

Tactic:
convert (reCLM : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))

Result:
case h.e'_10.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (⇑reCLM ∘ fun x => inner (id x) (id x)) x✝
-- Mathlib/Data/Int/Log.lean
theorem clog_zero_left (r : R) : clog 0 r = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
⊢ clog 0 r = 0

Tactic:
by_cases hr : 1 ≤ r

Result:
case pos
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ clog 0 r = 0

case neg
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ clog 0 r = 0

Proof state:
case neg
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ clog 0 r = 0

Tactic:
simp only [clog, hr, ite_cond_eq_false, Nat.log_zero_left, Nat.cast_zero, neg_zero]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ clog 0 r = 0

Tactic:
simp only [clog, Nat.clog_zero_left, Nat.cast_zero, Nat.log_zero_left, neg_zero, ite_self]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem union_right_iff : AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u

Tactic:
simp [union_eq_iUnion, and_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle_snd_fst_fst (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫
      pullback.fst _ _ = pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫
        t' 𝒰 f g j k i ≫
          t' 𝒰 f g k i j ≫
            pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
              pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫
      𝒰.map i =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫
      𝒰.map i

Tactic:
simp only [pullback.condition_assoc, t'_snd_fst_fst, t'_fst_snd, t'_snd_snd]

Result:
no goals

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g

Tactic:
rw [← cancel_mono (𝒰.map i)]

Result:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫
        t' 𝒰 f g j k i ≫
          t' 𝒰 f g k i j ≫
            pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
              pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫
      𝒰.map i =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫
      𝒰.map i
-- Mathlib/LinearAlgebra/Semisimple.lean
theorem IsSemisimple.aeval (p : K[X]) : (aeval f p).IsSemisimple :=
  let R := K[X] ⧸ Ideal.span {minpoly K f}
  have : Module.Finite K R :=
    (AdjoinRoot.powerBasis' <| minpoly.monic <| Algebra.IsIntegral.isIntegral f).finite
  have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
  isSemisimple_of_squarefree_aeval_eq_zero ((minpoly.isRadical K _).squarefree <|
    minpoly.ne_zero <| .of_finite K <| Ideal.Quotient.mkₐ K (.span {minpoly K f}) p) <| by
      rw [← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
        fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h, aeval_algHom,
        AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
a : K[X]
h : a ∈ Ideal.span {minpoly K f}
⊢ (aeval f) a = 0

Tactic:
rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (aeval ((aeval f) p)) (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) = 0

Tactic:
rw [← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
  fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h, aeval_algHom,
  AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem le_mk_of_comm {B A : C} {X : Subobject B} {f : A ⟶ B} [Mono f] (g : (X : C) ⟶ A)
    (w : g ≫ f = X.arrow) : X ≤ mk f :=
  le_of_comm (g ≫ (underlyingIso f).inv) <| by simp [w]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
g : underlying.obj X ⟶ A
w : g ≫ f = X.arrow
⊢ (g ≫ (underlyingIso f).inv) ≫ (mk f).arrow = X.arrow

Tactic:
simp [w]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem Subsequent.mk_right' (xL : xl → PGame) (xR : xr → PGame) (j : RightMoves (mk xl xr xL xR)) :
    Subsequent (xR j) (mk xl xr xL xR)

Proof state:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
j : (mk xl xr xL xR).RightMoves
⊢ (xR j).Subsequent (mk xl xr xL xR)

Tactic:
pgame_wf_tac

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma finitary_iff_forall_isCircuit_finite : M.Finitary ↔ ∀ C, M.IsCircuit C → C.Finite

Proof state:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.IsCircuit C
⊢ False

Tactic:
exact hC.dep.not_indep <| hI _ hCI (h C hC)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite

Tactic:
refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
  ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I

Tactic:
simpa

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

Tactic:
obtain ⟨C, hCI, hC⟩ := hd.exists_isCircuit_subset

Result:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.IsCircuit C
⊢ False

Proof state:
case refine_2
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

Tactic:
simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
@[to_additive addCentralizer_union]
lemma centralizer_union : centralizer (S ∪ T) = centralizer S ∩ centralizer T

Proof state:
M : Type u_1
S T : Set M
inst✝ : Mul M
⊢ (S ∪ T).centralizer = S.centralizer ∩ T.centralizer

Tactic:
simp [centralizer, or_imp, forall_and, setOf_and]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set E} :
    IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ i, IsVonNBounded 𝕜 (s i)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : SMul 𝕜 E
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ι : Sort u_6
inst✝ : Finite ι
s : ι → Set E
⊢ IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)

Tactic:
simp only [IsVonNBounded, absorbs_iUnion, @forall_swap ι]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.tendstoUniformlyOn {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r)
    (h : (r' : ℝ≥0∞) < r) :
    TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
      (Metric.ball (0 : E) r')

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (Metric.ball 0 ↑r')

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (Metric.ball 0 ↑r')

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (Metric.ball 0 ↑r')

Tactic:
simpa using hf.tendstoUniformlyOn h

Result:
no goals
-- Mathlib/RingTheory/Localization/Submodule.lean
theorem coeSubmodule_span (s : Set R) :
    coeSubmodule S (Ideal.span s) = Submodule.span R (algebraMap R S '' s)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ Submodule.span R (⇑(Algebra.linearMap R S) '' s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]

Result:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ Submodule.span R (⇑(Algebra.linearMap R S) '' s) = Submodule.span R (⇑(algebraMap R S) '' s)
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem id_base (X : Grothendieck F) :
    Hom.base (𝟙 X) = 𝟙 X.base

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (𝟙 X).base = 𝟙 X.base

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem one_le_iff_zero_lt {x : WithBot ℕ} : 1 ≤ x ↔ 0 < x

Proof state:
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x

Tactic:
cases x

Result:
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥

case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Proof state:
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
  ← WithBot.coe_le_coe, WithBot.coe_one] at h

Result:
no goals

Proof state:
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥

Tactic:
exact (not_lt_bot h).elim

Result:
no goals

Proof state:
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x

Tactic:
refine ⟨zero_lt_one.trans_le, fun h => ?_⟩

Result:
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_eq_zero (i : Δ' ⟶ Δ) [Mono i] (h₁ : Δ ≠ Δ') (h₂ : ¬Isδ₀ i) : mapMono K i = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Tactic:
rw [Ne] at h₁

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Tactic:
split_ifs

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ 0 = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ mapMono K i = 0

Tactic:
unfold mapMono

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem isReal_or_isComplex (w : InfinitePlace K) : IsReal w ∨ IsComplex w

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal

Tactic:
exact em _

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ w.IsComplex

Tactic:
rw [← not_isReal_iff_isComplex]

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal
-- Mathlib/NumberTheory/FLT/Four.lean
theorem Int.isCoprime_of_sq_sum' {r s : ℤ} (h : IsCoprime r s) :
    IsCoprime (r ^ 2 + s ^ 2) (r * s)

Proof state:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s

Tactic:
rw [add_comm]

Result:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s

Proof state:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s

Tactic:
apply Int.isCoprime_of_sq_sum h

Result:
no goals

Proof state:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) (r * s)

Tactic:
apply IsCoprime.mul_right (Int.isCoprime_of_sq_sum (isCoprime_comm.mp h))

Result:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essSup_uniformOn_eq_ciSup [Finite α] (hf : BddAbove (Set.range f)) :
    essSup f (uniformOn univ) = ⨆ a, f a :=
  essSup_eq_ciSup (by simpa [uniformOn, cond_apply]) hf

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝³ : ConditionallyCompleteLattice β
f : α → β
inst✝² : Nonempty α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Finite α
hf : BddAbove (range f)
⊢ ∀ (a : α), (uniformOn univ) {a} ≠ 0

Tactic:
simpa [uniformOn, cond_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem hasSum_iff (f : α → 𝕜) (c : 𝕜) :
    HasSum f c ↔ HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c)

Proof state:
case intro
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => re (f x)) (re c)
h₂ : HasSum (fun x => im (f x)) (im c)
⊢ HasSum f c

Tactic:
simpa only [re_add_im] using
  ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c) → HasSum f c

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case intro
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => re (f x)) (re c)
h₂ : HasSum (fun x => im (f x)) (im c)
⊢ HasSum f c

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum f c ↔ HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c)

Tactic:
refine ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, ?_⟩

Result:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => re (f x)) (re c) ∧ HasSum (fun x => im (f x)) (im c) → HasSum f c
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.sub {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s)
    (hg : LSeriesSummable g s) :
    LSeriesSummable (f - g) s

Proof state:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f - g) s

Tactic:
simpa [LSeriesSummable, ← term_sub_apply] using Summable.sub hf hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.IsExtensionBy_trans_right (state1 : State aig) (state2 : State aig)
    (state3 : State aig) (h12 : IsExtensionBy state1 state2 new1 hnew1)
    (h23 : IsExtensionBy state2 state3 new2 hnew2) : IsExtensionBy state1 state3 new2 hnew2

Proof state:
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.IsExtensionBy state3 new2 hnew2

Tactic:
apply  Cache.IsExtensionBy_trans_right

Result:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 ?new1 ?hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache.IsExtensionBy ?cache2 state3.cache new2 hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew1
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new1 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2

Proof state:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 ?new1 ?hnew1

Tactic:
exact h12

Result:
no goals

Proof state:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache new2 hnew2

Tactic:
exact h23

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sign_mul (x y : EReal) : sign (x * y) = sign x * sign y

Proof state:
case symm
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (y✝ * x✝) = sign y✝ * sign x✝

Tactic:
rwa [mul_comm, EReal.mul_comm]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ sign (⊤ * ↑x✝) = sign ⊤ * sign ↑x✝

Tactic:
rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]

Result:
no goals

Proof state:
case top_top

⊢ sign (⊤ * ⊤) = sign ⊤ * sign ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case coe_coe
x✝ y✝ : ℝ
⊢ sign (↑x✝ * ↑y✝) = sign ↑x✝ * sign ↑y✝

Tactic:
simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]

Result:
no goals

Proof state:
case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (-x✝ * y✝) = sign (-x✝) * sign y✝

Tactic:
rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

Result:
no goals

Proof state:
x y : EReal
⊢ sign (x * y) = sign x * sign y

Tactic:
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, sign_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

Result:
no goals

Proof state:
case top_zero

⊢ sign (⊤ * 0) = sign ⊤ * sign 0

Tactic:
simp only [zero_mul, mul_zero, sign_zero]

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem ringConGen_of_ringCon (c : RingCon R) : ringConGen c = c :=
  le_antisymm (by rw [ringConGen_eq]; exact sInf_le fun _ _ => id) RingConGen.Rel.of

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ ringConGen ⇑c ≤ c

Tactic:
rw [ringConGen_eq]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ sInf {s | ∀ (x y : R), c x y → s x y} ≤ c

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ sInf {s | ∀ (x y : R), c x y → s x y} ≤ c

Tactic:
exact sInf_le fun _ _ => id

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem lowerClosure_mul : ↑(lowerClosure s) * t = lowerClosure (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))

Tactic:
exact mul_lowerClosure _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))

Tactic:
simp_rw [mul_comm _ t]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.map_finset_sup [SemilatticeSup β] [OrderBot β]
    [FunLike F α β] [SupBotHomClass F α β]
    (f : F) (s : Finset ι) (g : ι → α) : f (s.sup g) = s.sup (f ∘ g) :=
  Finset.cons_induction_on s (map_bot f) fun i s _ h => by
    rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f ((cons i s x✝).sup g) = (cons i s x✝).sup (⇑f ∘ g)

Tactic:
rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

Result:
no goals