harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_mk_segment_left (x₁ x₂ : E) (y : F) :
    (fun x => (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x, y)) '' [x₁-[𝕜]x₂] = [(x₁, y)-[𝕜](x₂, y)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ (a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)

Tactic:
simp [Convex.combo_self ha.2.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem decide_forall_mem {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
    decide (∀ x, x ∈ xs → p x) = xs.all p

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), x ∈ xs → p x) = xs.all fun b => decide (p b)

Tactic:
simp [all_eq']

Result:
no goals
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem OrderedCommGroup.toMulRightReflectLE (α : Type u) [OrderedCommGroup α] :
    MulRightReflectLE α where
      elim a b c bc

Proof state:
α : Type u
inst✝ : OrderedCommGroup α
a b c : α
bc : swap (fun x1 x2 => x1 * x2) a b ≤ swap (fun x1 x2 => x1 * x2) a c
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_right' bc a⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n

Proof state:
x : Int
n : Nat
⊢ (x % ↑n).bmod n = x.bmod n

Tactic:
simp [bmod, Int.emod_emod]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_single_zero_smul {Γ} [OrderedAddCommMonoid Γ] [AddAction Γ Γ']
    [IsOrderedCancelVAdd Γ Γ'] [MulZeroClass R] [SMulWithZero R V] {r : R}
    {x : HahnModule Γ' R V} {a : Γ'} :
    ((of R).symm ((HahnSeries.single 0 r : HahnSeries Γ R) • x)).coeff a =
    r • ((of R).symm x).coeff a

Proof state:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ ((of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((of R).symm x).coeff a

Tactic:
nth_rw 1 [← zero_vadd Γ a]

Result:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ ((of R).symm ((HahnSeries.single 0) r • x)).coeff (0 +ᵥ a) = r • ((of R).symm x).coeff a

Proof state:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ ((of R).symm ((HahnSeries.single 0) r • x)).coeff (0 +ᵥ a) = r • ((of R).symm x).coeff a

Tactic:
exact coeff_single_smul_vadd

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Units.lean
theorem coeff_coe_units_zero_ne_zero [Nontrivial R] (u : R[X]ˣ) : coeff (u : R[X]) 0 ≠ 0

Proof state:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).coeff 0 ≠ 0

Tactic:
conv in 0 => rw [← natDegree_coe_units u]

Result:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).coeff (↑u).natDegree ≠ 0

Proof state:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0

Tactic:
exact Units.ne_zero _

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).coeff (↑u).natDegree ≠ 0

Tactic:
rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]

Result:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0
-- Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
theorem contDiff_piLp : ContDiff 𝕜 n f ↔ ∀ i, ContDiff 𝕜 n fun x => f x i

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff 𝕜 n fun x => f x i

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
-- Mathlib/CategoryTheory/Sites/SheafHom.lean
/-- Equational lemma for the presheaf structure on `presheafHom`.
It is advisable to use this lemma rather than `dsimp [presheafHom]` which may result
in the need to prove equalities of objects in an `Over` category. -/
lemma presheafHom_map_app {X Y Z : C} (f : Z ⟶ Y) (g : Y ⟶ X) (h : Z ⟶ X) (w : f ≫ g = h)
    (α : (presheafHom F G).obj (op X)) :
    ((presheafHom F G).map g.op α).app (op (Over.mk f)) =
      α.app (op (Over.mk h))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
h : Z ⟶ X
w : f ≫ g = h
α : (presheafHom F G).obj (op X)
⊢ ((presheafHom F G).map g.op α).app (op (Over.mk f)) = α.app (op (Over.mk h))

Tactic:
subst w

Result:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ ((presheafHom F G).map g.op α).app (op (Over.mk f)) = α.app (op (Over.mk (f ≫ g)))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ ((presheafHom F G).map g.op α).app (op (Over.mk f)) = α.app (op (Over.mk (f ≫ g)))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
@[simp]
lemma count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1

Proof state:
n : ℕ
a : Fin n
⊢ count a (finRange n) = 1

Tactic:
simp [count_eq_of_nodup (nodup_finRange n)]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma iSup_add_iSup_le [Nonempty ι] [Nonempty κ] {g : κ → ℝ≥0∞} (h : ∀ i j, f i + g j ≤ a) :
    iSup f + iSup g ≤ a

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a

Tactic:
exact iSup₂_le h

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
/-- `f` is Lipschitz iff it is Lipschitz on the entire space. -/
@[simp] lemma lipschitzOnWith_univ : LipschitzOnWith K f univ ↔ LipschitzWith K f

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f univ ↔ LipschitzWith K f

Tactic:
simp [LipschitzOnWith, LipschitzWith]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
lemma prod_norm_eq_idemFst_of_L1 (x : WithLp 1 (α × β)) : ‖x‖ = ‖idemFst x‖ + ‖idemSnd x‖

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ (‖idemFst x‖ ^ ENNReal.toReal 1 + ‖idemSnd x‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖idemFst x‖ + ‖idemSnd x‖

Tactic:
simp only [one_toReal, Real.rpow_one, ne_eq, one_ne_zero, not_false_eq_true, div_self]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖idemFst x‖ + ‖idemSnd x‖

Tactic:
rw [prod_norm_eq_add_idemFst (lt_of_lt_of_eq zero_lt_one one_toReal.symm)]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ (‖idemFst x‖ ^ ENNReal.toReal 1 + ‖idemSnd x‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖idemFst x‖ + ‖idemSnd x‖
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
    (a : α) {g : β × γ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂(κ ×ₖ η) a = ∫⁻ b, ∫⁻ c, g (b, c) ∂η a ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a

Tactic:
simp_rw [prod, lintegral_compProd _ _ _ hg, swapLeft_apply, prodMkLeft_apply, Prod.swap_prod_mk]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_integral_le (hf : Integrable f μ) : ∃ x, ∫ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [average_eq_integral] using exists_average_le (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem add_bddBelow_range_add {p q : NonarchAddGroupSeminorm E} {x : E} :
    BddBelow (range fun y => p y + q (x - y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩

Proof state:
case intro
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => p y + q (x - y))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => p y + q (x✝ - y)) x

Proof state:
case intro
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => p y + q (x✝ - y)) x

Tactic:
dsimp

Result:
case intro
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'
    (S : IntermediateField F K) [Algebra.IsAlgebraic F S] [IsPurelyInseparable F E] :
    sepDegree E (adjoin E (S : Set K)) = sepDegree F S

Proof state:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Tactic:
have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self]

Result:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Proof state:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this✝ : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
this : sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Tactic:
rwa [adjoin_self] at this

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Tactic:
have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set K)

Result:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this✝ : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
this : sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Proof state:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
⊢ Algebra.IsAlgebraic F ↥(adjoin F ↑S)

Tactic:
rwa [adjoin_self]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
    closedCell n j ⊆ skeletonLT C (n + 1)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ n < n + 1

Tactic:
exact lt_add_one n

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ↑n < ↑n + 1

Tactic:
norm_cast

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ n < n + 1

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Tactic:
simp_rw [mem_iUnion, exists_prop]

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ∃ i, ↑i < ↑n + 1 ∧ ∃ i_1, x ∈ closedCell i i_1

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ skeletonLT C (↑n + 1)

Tactic:
right

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ skeletonLT C (↑n + 1)

Tactic:
intro x xmem

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ skeletonLT C (↑n + 1)

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ∃ i, ↑i < ↑n + 1 ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N}
    {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
    (h : RootPairing.Equiv P₂ P₃) (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) :
    comp (comp h g) f = comp h (comp g f)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup N₁
inst✝⁸ : Module R N₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Cast.lean
theorem cast_choose_two (a : ℕ) : (a.choose 2 : K) = a * (a - 1) / 2

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a : ℕ
⊢ ↑(a.choose 2) = ↑a * (↑a - 1) / 2

Tactic:
rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
  cast_mul, cast_two, eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem C_dvd_iff_map_hom_eq_zero (q : R →+* S₁) (r : R) (hr : ∀ r' : R, q r' = 0 ↔ r ∣ r')
    (φ : MvPolynomial σ R) : C r ∣ φ ↔ map q φ = 0

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ ∀ (m : σ →₀ ℕ), coeff m ((map q) φ) = coeff m 0

Tactic:
simp only [coeff_map, coeff_zero, hr]

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ (map q) φ = 0

Tactic:
rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ ∀ (m : σ →₀ ℕ), coeff m ((map q) φ) = coeff m 0
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_choose {n k b : ℕ} [hp : Fact p.Prime] (hkn : k ≤ n) (hnb : log p n < b) :
    padicValNat p (choose n k) =
    ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card

Proof state:
p n k b : ℕ
hp : Fact (Nat.Prime p)
hkn : k ≤ n
hnb : log p n < b
⊢ padicValNat p (n.choose k) = (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card

Tactic:
exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| choose_pos hkn) ▸
  Prime.emultiplicity_choose hp.out hkn hnb

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_one_iff (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rw [ncard_le_one hs]

Result:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
tauto

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_eq_arccos_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, angle_add_eq_arccos_of_inner_eq_zero h]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_C : coeff (C a) n = ite (n = 0) a 0

Proof state:
case h.e'_3.h₁.a
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ n = 0 ↔ 0 = n

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
convert coeff_monomial (a := a) (m := n) (n := 0) using 2

Result:
case h.e'_3.h₁.a
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ n = 0 ↔ 0 = n
-- Mathlib/Algebra/Lie/Free.lean
theorem Rel.subRight {a b : lib R X} (c : lib R X) (h : Rel R X a b) : Rel R X (a - c) (b - c)

Proof state:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X a b
⊢ Rel R X (a - c) (b - c)

Tactic:
simpa only [sub_eq_add_neg] using h.add_right (-c)

Result:
no goals