harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma traceDual_top [Decidable (IsField A)] :
    (⊤ : Submodule B L)ᵛ = if IsField A then ⊤ else ⊥

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ ⊤ᵛ = if IsField A then ⊤ else ⊥

Tactic:
convert traceDual_top'

Result:
case h.e'_3.h₁.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ IsField A ↔ restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1

Proof state:
case h.e'_3.h₁.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ IsField A ↔ restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1

Tactic:
rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
  LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L),
  ← RingHom.range_eq_top, _root_.eq_top_iff]

Result:
case h.e'_3.h₁.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ ⊤ ≤ (algebraMap A K).range ↔ restrictScalars A ⊤ ≤ 1

Proof state:
case h.e'_3.h₁.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : Decidable (IsField A)
⊢ ⊤ ≤ (algebraMap A K).range ↔ restrictScalars A ⊤ ≤ 1

Tactic:
simp [SetLike.le_def]

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
    (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) :
    HasLiftingProperty i p ↔ HasLiftingProperty i' p

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i' p
⊢ HasLiftingProperty i p

Tactic:
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p

Tactic:
constructor <;> intro

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i' p
⊢ HasLiftingProperty i p
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem one_right : M.LinearDisjoint (1 : Submodule R S)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ Function.Injective ⇑(M.subtype ∘ₗ ↑M.rTensorOne)

Tactic:
exact M.injective_subtype.comp M.rTensorOne.injective

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ M.LinearDisjoint 1

Tactic:
rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_right_eq]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ Function.Injective ⇑(M.subtype ∘ₗ ↑M.rTensorOne)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_right_inj {x y : BitVec w} (z : BitVec w) : (z + x = z + y) ↔ x = y

Proof state:
w : Nat
x y z : BitVec w
⊢ z + x = z + y ↔ x = y

Tactic:
simp [BitVec.add_comm z]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_mul_closedBall_one : {x} * closedBall 1 δ = closedBall x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * closedBall 1 δ = closedBall x δ

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/List.lean
theorem continuous_insertIdx' {n : ℕ} {i : Fin (n + 1)} :
    Continuous fun p : α × List.Vector α n => Vector.insertIdx p.1 i p.2 :=
  continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by
    rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × List.Vector α n
a : α
l : List.Vector α n
⊢ ContinuousAt (fun p => Vector.insertIdx p.1 i p.2) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × List.Vector α n
a : α
l : List.Vector α n
⊢ Tendsto (fun p => Vector.insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (Vector.insertIdx (a, l).1 i (a, l).2))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × List.Vector α n
a : α
l : List.Vector α n
⊢ Tendsto (fun p => Vector.insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (Vector.insertIdx (a, l).1 i (a, l).2))

Tactic:
exact tendsto_insertIdx

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomial (P : Fin 3 → R) : eval P W'.polynomial =
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3
      - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomial =
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)

Tactic:
rw [polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)

Tactic:
eval_simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem le_bot_iff : ∀ {a : WithBot α}, a ≤ ⊥ ↔ a = ⊥
  | (a : α) => by simp [not_coe_le_bot _]
  | ⊥ => by simp

Proof state:
α : Type u_1
inst✝ : LE α
a : α
⊢ ↑a ≤ ⊥ ↔ ↑a = ⊥

Tactic:
simp [not_coe_le_bot _]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LE α
⊢ ⊥ ≤ ⊥ ↔ ⊥ = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Colimit/Ring.lean
lemma congr_symm_apply_of (e : (i : ι) → G i ≃+* G' i)
    (he : ∀ i j h, (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i))
    {i : ι} (g : G' i) :
    (congr e he).symm (of G' _ i g) = of G (fun _ _ h ↦ f _ _ h) i ((e i).symm g)

Proof state:
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i : ι
g : G' i
⊢ (congr e he).symm ((of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) g) = (of G (fun x x_1 h => ⇑(f x x_1 h)) i) ((e i).symm g)

Tactic:
simp only [congr, RingEquiv.ofRingHom_symm_apply, map_apply_of, RingHom.coe_coe]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) : W'.addY P Q = P y ^ 2 * Q z * Q y

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addY P Q = P y ^ 2 * Q z * Q y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_left hP hPz, negY, addX_of_Z_eq_zero_left hP hPz,
  addZ_of_Z_eq_zero_left hP hPz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) - W'.a₁ * (P y ^ 2 * Q z * Q x) -
      W'.a₃ * (P y ^ 2 * Q z * Q z) =
    P y ^ 2 * Q z * Q y

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) - W'.a₁ * (P y ^ 2 * Q z * Q x) -
      W'.a₃ * (P y ^ 2 * Q z * Q z) =
    P y ^ 2 * Q z * Q y

Tactic:
ring1

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma forall_congr (h : ∀ a, p a ↔ q (e a)) : (∀ a, p a) ↔ ∀ b, q b :=
  e.forall_congr_left.trans (by simp [h])

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem mul_geom_sum [Ring α] (x : α) (n : ℕ) : ((x - 1) * ∑ i ∈ range n, x ^ i) = x ^ n - 1 :=
  op_injective <| by simpa using geom_sum_mul (op x) n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((x - 1) * ∑ i ∈ range n, x ^ i) = op (x ^ n - 1)

Tactic:
simpa using geom_sum_mul (op x) n

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem primeSpectrumProd_symm_inr_asIdeal (x : PrimeSpectrum S) :
    ((primeSpectrumProd R S).symm <| Sum.inr x).asIdeal = Ideal.prod ⊤ x.asIdeal

Proof state:
case mk
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
asIdeal✝ : Ideal S
isPrime✝ : asIdeal✝.IsPrime
⊢ ((primeSpectrumProd R S).symm (Sum.inr { asIdeal := asIdeal✝, isPrime := isPrime✝ })).asIdeal =
    ⊤.prod { asIdeal := asIdeal✝, isPrime := isPrime✝ }.asIdeal

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
⊢ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal

Tactic:
cases x

Result:
case mk
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
asIdeal✝ : Ideal S
isPrime✝ : asIdeal✝.IsPrime
⊢ ((primeSpectrumProd R S).symm (Sum.inr { asIdeal := asIdeal✝, isPrime := isPrime✝ })).asIdeal =
    ⊤.prod { asIdeal := asIdeal✝, isPrime := isPrime✝ }.asIdeal
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_erase [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (s.erase i).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0

Tactic:
rw [vsub_self, smul_zero]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)

Tactic:
apply sum_erase

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_natCast (n : ℕ) : toPGame n ≈ n

Proof state:
n : ℕ
⊢ (↑n).toPGame ≈ ↑n

Tactic:
rw [PGame.equiv_iff_game_eq, mk_toPGame, toGame_natCast, quot_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Subalgebra.finrank_bot : finrank F (⊥ : Subalgebra F E) = 1 :=
  finrank_eq_of_rank_eq (by simp)

Proof state:
F : Type u_2
E : Type u_3
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F ↥⊥ = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_add' {m n : ℤ} {x : AddCircle T} :
    toCircle ((m + n) • x :) = fourier m x * fourier n x

Proof state:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x

Tactic:
rw [← fourier_apply]

Result:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Proof state:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Tactic:
exact fourier_add

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_span_singleton_trans {x y z : M} (hxy : x ∈ R ∙ y) (hyz : y ∈ R ∙ z) : x ∈ R ∙ z

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : {x} ⊆ ↑(span R {y})
hyz : {y} ⊆ ↑(span R {z})
⊢ {x} ⊆ ↑(span R {z})

Tactic:
exact Submodule.subset_span_trans hxy hyz

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : x ∈ span R {y}
hyz : y ∈ span R {z}
⊢ x ∈ span R {z}

Tactic:
rw [← SetLike.mem_coe, ← singleton_subset_iff] at *

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : {x} ⊆ ↑(span R {y})
hyz : {y} ⊆ ↑(span R {z})
⊢ {x} ⊆ ↑(span R {z})
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n

Proof state:
m n : Nat
⊢ m.gcd n * m.lcm n = m * n

Tactic:
rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitesimal_def {x : ℝ*} : Infinitesimal x ↔ ∀ r : ℝ, 0 < r → -(r : ℝ*) < x ∧ x < r

Proof state:
x : ℝ*
⊢ x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r

Tactic:
simp [Infinitesimal, IsSt]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem ContMDiffMul.of_le {m n : WithTop ℕ∞} (hmn : m ≤ n)
    [h : ContMDiffMul I n G] : ContMDiffMul I m G

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : WithTop ℕ∞
hmn : m ≤ n
h : ContMDiffMul I n G
this : IsManifold I m G
⊢ ContMDiffMul I m G

Tactic:
exact ⟨h.contMDiff_mul.of_le hmn⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : WithTop ℕ∞
hmn : m ≤ n
h : ContMDiffMul I n G
⊢ ContMDiffMul I m G

Tactic:
have : IsManifold I m G := IsManifold.of_le hmn

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : WithTop ℕ∞
hmn : m ≤ n
h : ContMDiffMul I n G
this : IsManifold I m G
⊢ ContMDiffMul I m G
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem projectSubobject_factors [HasFiniteLimits C] [PreservesFiniteLimits T]
    {A : StructuredArrow S T} :
    ∀ P : Subobject A, ∃ q, q ≫ T.map (projectSubobject P).arrow = A.hom :=
  Subobject.ind _ fun P f hf =>
    ⟨P.hom ≫ T.map (Subobject.underlyingIso _).inv, by
      dsimp
      simp [← T.map_comp]⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso (MonoOver.mk' f).arrow.right).inv) ≫
      T.map (projectSubobject (Subobject.mk f)).arrow =
    A.hom

Tactic:
dsimp

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.mk f.right).arrow = A.hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.mk f.right).arrow = A.hom

Tactic:
simp [← T.map_comp]

Result:
no goals
-- Mathlib/RingTheory/Presentation.lean
lemma ideal_fg_of_isFinite [P.IsFinite] : P.ker.FG

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Presentation R S
inst✝ : P.IsFinite
⊢ P.ker.FG

Tactic:
use (Set.finite_range P.relation).toFinset

Result:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Presentation R S
inst✝ : P.IsFinite
⊢ Ideal.span ↑⋯.toFinset = P.ker

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Presentation R S
inst✝ : P.IsFinite
⊢ Ideal.span ↑⋯.toFinset = P.ker

Tactic:
simp [span_range_relation_eq_ker]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
/-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
any `x : L`, `ad (D x)` is also in this orthogonal. -/
lemma ad_mem_orthogonal_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
    ad R L (D x) ∈ 𝕀ᗮ

Proof state:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ ⁅x, D⁆ ∈ (killingForm R (LieDerivation R L L)).orthogonal (LinearMap.range ↑(ad R L))

Tactic:
exact (rangeAdOrthogonal R L).lie_mem hD

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule

Tactic:
simp only [ad_apply_lieDerivation, LieHom.range_toSubmodule, neg_mem_iff]

Result:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ ⁅x, D⁆ ∈ (killingForm R (LieDerivation R L L)).orthogonal (LinearMap.range ↑(ad R L))
-- Mathlib/Probability/Moments/Basic.lean
theorem centralMoment_one' [IsFiniteMeasure μ] (h_int : Integrable X μ) :
    centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * μ[X]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [sub_mul, integral_const, smul_eq_mul, one_mul]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ

Tactic:
rw [integral_sub h_int (integrable_const _)]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m ≤ n) :
    a ^ (n - m) * a ^ m = a ^ n

Proof state:
a m n : Nat
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n

Tactic:
rw [← Nat.pow_add, Nat.sub_add_cancel h]

Result:
no goals