harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.induce_supp (c : G.ConnectedComponent) (h : G.IsCycles) :
    (G.induce c.supp).spanningCoe.IsCycles

Proof state:
case e_s.h
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
w' : V
⊢ w' ∈ (induce c.supp G).spanningCoe.neighborSet v ↔ w' ∈ G.neighborSet v

Tactic:
simp only [mem_neighborSet, c.adj_spanningCoe_induce_supp, hw, true_and]

Result:
no goals

Proof state:
case e_s
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (induce c.supp G).spanningCoe.neighborSet v = G.neighborSet v

Tactic:
ext w'

Result:
case e_s.h
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
w' : V
⊢ w' ∈ (induce c.supp G).spanningCoe.neighborSet v ↔ w' ∈ G.neighborSet v

Proof state:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : w ∈ (induce c.supp G).spanningCoe.neighborSet v
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = 2

Tactic:
rw [mem_neighborSet, c.adj_spanningCoe_induce_supp] at hw

Result:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = 2

Proof state:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = 2

Tactic:
rw [← h ⟨w, hw.2⟩]

Result:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = (G.neighborSet v).ncard

Proof state:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
⊢ (induce c.supp G).spanningCoe.IsCycles

Tactic:
intro v ⟨w, hw⟩

Result:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : w ∈ (induce c.supp G).spanningCoe.neighborSet v
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = 2

Proof state:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ ((induce c.supp G).spanningCoe.neighborSet v).ncard = (G.neighborSet v).ncard

Tactic:
congr

Result:
case e_s
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (induce c.supp G).spanningCoe.neighborSet v = G.neighborSet v
-- Mathlib/Topology/CompactOpen.lean
theorem Topology.IsQuotientMap.continuous_lift_prod_right (hf : IsQuotientMap f) {g : Y × X → Z}
    (hg : Continuous fun p : Y × X₀ => g (p.1, f p.2)) : Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.1, f p.2)
this : Continuous fun p => g (p.swap.1, f p.swap.2)
⊢ Continuous g

Tactic:
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.1, f p.2)
this✝ : Continuous fun p => g (p.swap.1, f p.swap.2)
this : Continuous fun p => (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.1, f p.2)
this✝ : Continuous fun p => g (p.swap.1, f p.swap.2)
this : Continuous fun p => (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous g

Tactic:
exact (hf.continuous_lift_prod_left this).comp continuous_swap

Result:
no goals

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.1, f p.2)
⊢ Continuous g

Tactic:
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
  hg.comp continuous_swap

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.1, f p.2)
this : Continuous fun p => g (p.swap.1, f p.swap.2)
⊢ Continuous g
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
/-- The range of the adjoint action on a finite-dimensional Killing Lie algebra is full. -/
@[simp]
lemma range_ad_eq_top : 𝕀 = ⊤

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
hD : D ∈ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ D x = 0 x

Tactic:
simpa using ad_mem_ker_killingForm_ad_range_of_mem_orthogonal hD x

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
hD : D ∈ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ D x = 0 x

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range = ⊤

Tactic:
rw [← LieSubalgebra.toSubmodule_inj]

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range.toSubmodule = ⊤.toSubmodule

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range.toSubmodule = ⊤.toSubmodule

Tactic:
apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
  (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = ⊥
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.closedBall_one_mul (hs : IsCompact s) (hδ : 0 ≤ δ) :
    closedBall 1 δ * s = cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s

Tactic:
rw [mul_comm, hs.mul_closedBall_one hδ]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_add {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (x + y).toENNReal = x.toENNReal + y.toENNReal

Proof state:
case h_real.h_real
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ENNReal.ofReal (a✝¹ + a✝) = ENNReal.ofReal a✝¹ + ENNReal.ofReal a✝

Tactic:
simp_all [ENNReal.ofReal_add]

Result:
no goals

Proof state:
case h_real.h_real
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
norm_cast

Result:
case h_real.h_real
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑(a✝¹ + a✝)).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Proof state:
case h_top.h_top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
simp_all

Result:
no goals

Proof state:
case h_real.h_real
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑(a✝¹ + a✝)).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
simp_rw [real_coe_toENNReal]

Result:
case h_real.h_real
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ENNReal.ofReal (a✝¹ + a✝) = ENNReal.ofReal a✝¹ + ENNReal.ofReal a✝
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem not_linearIndependent_pair_of_commute_of_flat_right [Module.Flat R N]
    (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) : ¬LinearIndependent R ![a, b] := fun h ↦ by
  let m : Fin 2 → M := (inclusion inf_le_left) ∘ ![a, b]
  have hm : LinearIndependent R m := h.map' _ (ker_inclusion _ _ _)
  -- need this instance otherwise it only has semigroup structure
  letI : AddCommGroup (Fin 2 →₀ N) := Finsupp.instAddCommGroup
  let n : Fin 2 →₀ N := .single 0 ⟨b.1, b.2.2⟩ - .single 1 ⟨a.1, a.2.2⟩
  have hn : mulLeftMap N m n = 0

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
⊢ False

Tactic:
let n : Fin 2 →₀ N := .single 0 ⟨b.1, b.2.2⟩ - .single 1 ⟨a.1, a.2.2⟩

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
⊢ False

Tactic:
have hm : LinearIndependent R m := h.map' _ (ker_inclusion _ _ _)

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ (mulLeftMap N m) n = 0

Tactic:
simp [m, n, show _ * _ = _ * _ from hc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/MinMax.lean
theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c

Proof state:
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
⊢ a ≤ min b c

Tactic:
cases Nat.le_total b c with
| inl h => rw [Nat.min_eq_left h]; assumption
| inr h => rw [Nat.min_eq_right h]; assumption

Result:
no goals

Proof state:
case inr
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : c ≤ b
⊢ a ≤ min b c

Tactic:
rw [Nat.min_eq_right h]

Result:
case inr
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : c ≤ b
⊢ a ≤ c

Proof state:
case inl
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : b ≤ c
⊢ a ≤ min b c

Tactic:
rw [Nat.min_eq_left h]

Result:
case inl
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : b ≤ c
⊢ a ≤ b

Proof state:
a b c : Nat
⊢ a ≤ b → a ≤ c → a ≤ min b c

Tactic:
intros

Result:
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
⊢ a ≤ min b c

Proof state:
case inl
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : b ≤ c
⊢ a ≤ b

Tactic:
assumption

Result:
no goals

Proof state:
case inr
a b c : Nat
a✝¹ : a ≤ b
a✝ : a ≤ c
h : c ≤ b
⊢ a ≤ c

Tactic:
assumption

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_factors' {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R}
    {J : Ideal R} (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
    ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite,
      ((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_nmem :
  (Associates.mk v.asIdeal).count (Associates.mk J).factors = 0 ∧
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0
⊢ False

Tactic:
rw [mem_setOf_eq, h_nmem.1, h_nmem.2, sub_self] at hv

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv : ¬0 = 0
hv_irred : Irreducible v.asIdeal
h_nmem :
  (Associates.mk v.asIdeal).count (Associates.mk J).factors = 0 ∧
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0
⊢ False
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_sub_Ioo : (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)

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

Tactic:
simp [← Ioi_inter_Iio, inter_comm]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
protected lemma add : IsAlgebraic R (a + b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Tactic:
exact (int_a.smul _).add (int_b.smul _)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a + b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a + b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((rb * ra) • (a + b))

Tactic:
rw [smul_add, mul_smul, mul_comm, mul_smul]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a + b)

Tactic:
refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((rb * ra) • (a + b))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem modify_eq_alter [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l : AssocList α β} :
    modify a f l = alter a (·.map f) l

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Tactic:
next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
⊢ modify a f nil = alter a (fun x => Option.map f x) nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
l : AssocList α β
⊢ modify a f l = alter a (fun x => Option.map f x) l

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
⊢ modify a f nil = alter a (fun x => Option.map f x) nil

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : β a → β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
ih : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Tactic:
simp only [modify, beq_iff_eq, alter, Option.map_some', ih]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem Balanced.subset_smul (hs : Balanced 𝕜 s) (ha : 1 ≤ ‖a‖) : s ⊆ a • s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
rw [← @norm_one 𝕜] at ha

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖1‖ ≤ ‖a‖
⊢ s ⊆ a • s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖1‖ ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
simpa using hs.smul_mono ha

Result:
no goals
-- Mathlib/FieldTheory/IsSepClosed.lean
theorem roots_eq_zero_iff [IsSepClosed k] {p : k[X]} (hsep : p.Separable) :
    p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

Proof state:
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Tactic:
obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep

Result:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ p = C (p.coeff 0)

Proof state:
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)

Tactic:
exact eq_C_of_degree_le_zero hd

Result:
no goals

Proof state:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ p = C (p.coeff 0)

Tactic:
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz

Result:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
⊢ p = C (p.coeff 0)

Tactic:
rcases le_or_lt (degree p) 0 with hd | hd

Result:
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)

case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Proof state:
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)

Tactic:
simp at hz

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
⊢ p.roots = 0 ↔ p = C (p.coeff 0)

Tactic:
refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩

Result:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
⊢ p = C (p.coeff 0)

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
hp : p = C (p.coeff 0)
⊢ p.roots = 0

Tactic:
rw [hp, roots_C]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma finset_sup_nhds_apply [SemilatticeSup L] [OrderBot L] [ContinuousSup L]
    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
    Tendsto (fun a ↦ s.sup (f · a)) l (𝓝 (s.sup g))

Proof state:
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a => s.sup fun x => f x a) l (𝓝 (s.sup g))

Tactic:
simpa only [← Finset.sup_apply] using finset_sup_nhds hs

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem disjoint_iff : Disjoint f g ↔ Disjoint f.support g.support

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
rw [disjoint_iff, disjoint_iff, DFinsupp.bot_eq_zero, ← DFinsupp.support_eq_empty,
  DFinsupp.support_inf]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥

Tactic:
rfl

Result:
no goals