harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_pos_of_isRat_neg {n : ℤ} :
    (NormNum.IsRat e n d) → (decide (n / d < (-1 : ℚ))) → (0 < Real.log (e : ℝ))
  | ⟨inv, eq⟩, h => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : (n : ℝ) / d < -1

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ ↑n / ↑d < -1

Tactic:
exact_mod_cast of_decide_eq_true h

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
exact Real.log_pos_of_lt_neg_one this

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closure_subset_cthickening (δ : ℝ) (E : Set α) : closure E ⊆ cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (δ ⊓ 0) E ⊆ cthickening δ E

Tactic:
exact cthickening_mono (min_le_left δ 0) E

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ closure E ⊆ cthickening δ E

Tactic:
rw [← cthickening_of_nonpos (min_le_right δ 0)]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (δ ⊓ 0) E ⊆ cthickening δ E
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_exp_one (x : ℝ) : angle (exp (x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|

Proof state:
x : ℝ
⊢ angle (cexp (↑x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|

Tactic:
simpa using angle_exp_exp x 0

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem finrank_range_dualMap_eq_finrank_range (f : V₁ →ₗ[K] V₂) :
    finrank K (LinearMap.range f.dualMap) = finrank K (LinearMap.range f)

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f = (range f).subtype ∘ₗ f.rangeRestrict

Tactic:
rfl

Result:
no goals

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥(range f.dualMap) = finrank K ↥(range f)

Tactic:
rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl),
  ← dualMap_comp_dualMap, range_comp,
  range_eq_top.mpr (dualMap_surjective_of_injective (range f).injective_subtype),
  Submodule.map_top, finrank_range_of_inj, Subspace.dual_finrank_eq]

Result:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ⇑f.rangeRestrict.dualMap

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ⇑f.rangeRestrict.dualMap

Tactic:
exact dualMap_injective_of_surjective (range_eq_top.mp f.range_rangeRestrict)

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem eqToHom_left {X Y : CostructuredArrow S T} (h : X = Y) :
    (eqToHom h).left = eqToHom (by rw [h])

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' Y'' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, id_left]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom ⋯).left = eqToHom ⋯
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_monomial (s : σ →₀ ℕ) (a : R) : degrees (monomial s a) ≤ toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ ((monomial s) a).degrees ≤ toMultiset s

Tactic:
classical
  refine (supDegree_single s a).trans_le ?_
  split_ifs
  exacts [bot_le, le_rfl]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ ((monomial s) a).degrees ≤ toMultiset s

Tactic:
refine (supDegree_single s a).trans_le ?_

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ (if a = 0 then ⊥ else toMultiset s) ≤ toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ (if a = 0 then ⊥ else toMultiset s) ≤ toMultiset s

Tactic:
split_ifs

Result:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : a = 0
⊢ ⊥ ≤ toMultiset s

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : ¬a = 0
⊢ toMultiset s ≤ toMultiset s

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : a = 0
⊢ ⊥ ≤ toMultiset s

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : ¬a = 0
⊢ toMultiset s ≤ toMultiset s

Tactic:
exacts [bot_le, le_rfl]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
@[simp]
lemma indicatorConstLp_univ :
    indicatorConstLp p .univ (measure_ne_top μ _) c = Lp.const p μ c

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ MemLp.toLp (Set.univ.indicator fun x => c) ⋯ = MemLp.toLp (fun x => c) ⋯

Tactic:
simp only [Set.indicator_univ, Function.const]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = (Lp.const p μ) c

Tactic:
rw [← MemLp.toLp_const, indicatorConstLp]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ MemLp.toLp (Set.univ.indicator fun x => c) ⋯ = MemLp.toLp (fun x => c) ⋯
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp₂_toGerm (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β)
    (f₂ : α →ₘ[μ] γ) : (comp₂ g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm :=
  induction_on₂ f₁ f₂ fun f₁ _ f₂ _ => by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁✝ : α →ₘ[μ] β
f₂✝ : α →ₘ[μ] γ
f₁ : α → β
x✝¹ : AEStronglyMeasurable f₁ μ
f₂ : α → γ
x✝ : AEStronglyMeasurable f₂ μ
⊢ (comp₂ g hg (mk f₁ x✝¹) (mk f₂ x✝)).toGerm = Germ.map₂ g (mk f₁ x✝¹).toGerm (mk f₂ x✝).toGerm

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negDblY_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.negDblY P = -W.dblU P

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.negDblY P = -W.dblU P

Tactic:
rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
  mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_eq_div {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k

Proof state:
δ : Type u_3
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k

Tactic:
simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem prodEquivOfIsCompl_symm_apply_left (h : IsCompl p q) (x : p) :
    (prodEquivOfIsCompl p q h).symm x = (x, 0) :=
  (prodEquivOfIsCompl p q h).symm_apply_eq.2 <| by simp

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥p
⊢ ↑x = (p.prodEquivOfIsCompl q h) (x, 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem Nat.cast_npow (R : Type*) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n m : ℕ) :
    (↑(n ^ m) : R) = (↑n : R) ^ m

Proof state:
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m

Tactic:
induction m with
| zero => simp only [pow_zero, Nat.cast_one, npow_zero]
| succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ (m + 1)) = ↑n ^ (m + 1)

Tactic:
rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℕ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
simp only [pow_zero, Nat.cast_one, npow_zero]

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem equiv_or_fuzzy_zero : G ≈ 0 ∨ G ‖ 0

Proof state:
case inr.inl
G : PGame
inst✝ : G.Impartial
h : G ≈ 0
⊢ G ≈ 0 ∨ G ‖ 0

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case inr.inr.inr
G : PGame
inst✝ : G.Impartial
h : G ‖ 0
⊢ G ≈ 0 ∨ G ‖ 0

Tactic:
exact Or.inr h

Result:
no goals

Proof state:
case inl
G : PGame
inst✝ : G.Impartial
h : G < 0
⊢ G ≈ 0 ∨ G ‖ 0

Tactic:
exact ((nonneg G) h).elim

Result:
no goals

Proof state:
case inr.inr.inl
G : PGame
inst✝ : G.Impartial
h : 0 < G
⊢ G ≈ 0 ∨ G ‖ 0

Tactic:
exact ((nonpos G) h).elim

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G ≈ 0 ∨ G ‖ 0

Tactic:
rcases lt_or_equiv_or_gt_or_fuzzy G 0 with (h | h | h | h)

Result:
case inl
G : PGame
inst✝ : G.Impartial
h : G < 0
⊢ G ≈ 0 ∨ G ‖ 0

case inr.inl
G : PGame
inst✝ : G.Impartial
h : G ≈ 0
⊢ G ≈ 0 ∨ G ‖ 0

case inr.inr.inl
G : PGame
inst✝ : G.Impartial
h : 0 < G
⊢ G ≈ 0 ∨ G ‖ 0

case inr.inr.inr
G : PGame
inst✝ : G.Impartial
h : G ‖ 0
⊢ G ≈ 0 ∨ G ‖ 0
-- Mathlib/Data/ZMod/ValMinAbs.lean
@[simp]
lemma natAbs_valMinAbs_neg (a : ZMod n) : (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Proof state:
n : ℕ
a : ZMod n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
by_cases h2a : 2 * a.val = n

Result:
case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Proof state:
case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rw [a.neg_eq_self_iff.2 (Or.inr h2a)]

Result:
no goals

Proof state:
case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem continuousEvalConst [TopologicalSpace F] [IsTopologicalAddGroup F]
    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
    ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F where
  continuous_eval_const x

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
⊢ Continuous fun f => f x

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ Continuous fun f => f x

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ Continuous fun f => f x

Tactic:
haveI : UniformAddGroup F := uniformAddGroup_of_addCommGroup

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous fun f => f x

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous fun f => f x

Tactic:
exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
  (isEmbedding_coeFn σ F 𝔖).continuous

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
lemma isCompl_ker_of_disjoint_of_ne_bot {p : Submodule K V₁}
    (hpf : Disjoint (LinearMap.ker f) p) (hp : p ≠ ⊥) :
    IsCompl (LinearMap.ker f) p

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p

Tactic:
simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Tactic:
have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
  simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]

Result:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p

Tactic:
refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩

Result:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Tactic:
rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
  Submodule.one_le_finrank_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem copy_copy {u v u' v' u'' v''} (p : G.Walk u v)
    (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
    (p.copy hu hv).copy hu' hv' = p.copy (hu.trans hu') (hv.trans hv')

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' u'' v'' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ (p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u'' v'' : V
p : G.Walk u'' v''
⊢ (p.copy ⋯ ⋯).copy ⋯ ⋯ = p.copy ⋯ ⋯

Proof state:
V : Type u
G : SimpleGraph V
u'' v'' : V
p : G.Walk u'' v''
⊢ (p.copy ⋯ ⋯).copy ⋯ ⋯ = p.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem filtration_succ (i : ι) : E⟮<i⁺⟯ = E⟮<i⟯⟮b (φ i)⟯.restrictScalars F

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ adjoin F (⇑b ∘ φ '' Iio i ∪ {(⇑b ∘ φ) i}) = adjoin F (⇑b ∘ φ '' Iio i ∪ {b (φ i)})

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ adjoin F (⇑b ∘ φ '' Iio (i⁺)) = restrictScalars F (↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Tactic:
rw [Iio_succ, ← Iio_insert, image_insert_eq, ← union_singleton, adjoin_adjoin_left]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ adjoin F (⇑b ∘ φ '' Iio i ∪ {(⇑b ∘ φ) i}) = adjoin F (⇑b ∘ φ '' Iio i ∪ {b (φ i)})
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem quasiCompact_iff_spectral : QuasiCompact f ↔ IsSpectralMap f.base :=
  ⟨fun ⟨h⟩ => ⟨by fun_prop, h⟩, fun h => ⟨h.2⟩⟩

Proof state:
X Y : Scheme
f : X ⟶ Y
x✝ : QuasiCompact f
h : ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)
⊢ Continuous ⇑(ConcreteCategory.hom f.base)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.mul {f g : R[X]} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) :
    (f * g).Separable

Proof state:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative f * g + f * derivative g)

Tactic:
exact
  ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable

Tactic:
rw [separable_def, derivative_mul]

Result:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative f * g + f * derivative g)
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem {s : AffineSubspace k P} {p₁ p₂ p₃ : P}
    (hp₂p₃ : p₂ ≠ p₃) (hp₁ : p₁ ∉ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) :
    AffineIndependent k ![p₁, p₂, p₃]

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2))

Tactic:
convert affineIndependent_of_ne_of_mem_of_mem_of_not_mem hp₂p₃.symm hp₃ hp₂ hp₁ using 1

Result:
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2) = ![p₃, p₂, p₁]

Proof state:
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2)) x = ![p₃, p₂, p₁] x

Tactic:
fin_cases x <;> rfl

Result:
no goals

Proof state:
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2) = ![p₃, p₂, p₁]

Tactic:
ext x

Result:
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2)) x = ![p₃, p₂, p₁] x
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFold_eq_fold (s : Multiset α) [Std.Commutative op] (a : α) :
    noncommFold op s (fun x _ y _ _ => Std.Commutative.comm x y) a = fold op a s

Proof state:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
inst✝ : Std.Commutative op
a : α
⊢ noncommFold op s ⋯ a = fold op a s

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
inst✝ : Std.Commutative op
a : α
a✝ : List α
⊢ noncommFold op ⟦a✝⟧ ⋯ a = fold op a ⟦a✝⟧

Proof state:
case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
inst✝ : Std.Commutative op
a : α
a✝ : List α
⊢ noncommFold op ⟦a✝⟧ ⋯ a = fold op a ⟦a✝⟧

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem le_of_sub_le_sub_left : ∀ {n k m : Nat}, n ≤ k → k - m ≤ k - n → n ≤ m
  | 0, _, _, _, _ => Nat.zero_le ..
  | _+1, _, 0, h₀, h₁ =>
    absurd (Nat.sub_lt (Nat.zero_lt_of_lt h₀) (Nat.zero_lt_succ _)) (Nat.not_lt.2 h₁)
  | _+1, _+1, _+1, h₀, h₁ => by
    simp only [Nat.succ_sub_succ] at h₁
    exact succ_le_succ <| Nat.le_of_sub_le_sub_left (Nat.le_of_succ_le_succ h₀) h₁

Proof state:
n✝² n✝¹ n✝ : Nat
h₀ : n✝² + 1 ≤ n✝¹ + 1
h₁ : n✝¹ - n✝ ≤ n✝¹ - n✝²
⊢ n✝² + 1 ≤ n✝ + 1

Tactic:
exact succ_le_succ <| Nat.le_of_sub_le_sub_left (Nat.le_of_succ_le_succ h₀) h₁

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
h₀ : n✝² + 1 ≤ n✝¹ + 1
h₁ : n✝¹ + 1 - (n✝ + 1) ≤ n✝¹ + 1 - (n✝² + 1)
⊢ n✝² + 1 ≤ n✝ + 1

Tactic:
simp only [Nat.succ_sub_succ] at h₁

Result:
n✝² n✝¹ n✝ : Nat
h₀ : n✝² + 1 ≤ n✝¹ + 1
h₁ : n✝¹ - n✝ ≤ n✝¹ - n✝²
⊢ n✝² + 1 ≤ n✝ + 1