harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_append {s t : Array α} {i : Nat} {x : α} (h : i < (s ++ t).size) :
    (s ++ t).set i x =
      if h' : i < s.size then
        s.set i x ++ t
      else
        s ++ t.set (i - s.size) x (by simp at h; omega)

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
h : i < ({ toList := s } ++ { toList := t }).size
⊢ ({ toList := s } ++ { toList := t }).set i x h =
    if h' : i < { toList := s }.size then { toList := s }.set i x h' ++ { toList := t }
    else { toList := s } ++ { toList := t }.set (i - { toList := s }.size) x ⋯

Tactic:
simp only [List.append_toArray, List.set_toArray, List.set_append]

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
h : i < ({ toList := s } ++ { toList := t }).size
⊢ (if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x).toArray =
    if h : i < { toList := s }.size then (s.set i x ++ t).toArray else (s ++ t.set (i - { toList := s }.size) x).toArray

Proof state:
α : Type ?u.246537
s t : Array α
i : Nat
x : α
h : i < (s ++ t).size
h' : ¬i < s.size
⊢ i - s.size < t.size

Tactic:
simp at h

Result:
α : Type ?u.246537
s t : Array α
i : Nat
x : α
h' : ¬i < s.size
h : i < s.size + t.size
⊢ i - s.size < t.size

Proof state:
α : Type ?u.246537
s t : Array α
i : Nat
x : α
h' : ¬i < s.size
h : i < s.size + t.size
⊢ i - s.size < t.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h : i < (s ++ t).size
⊢ (s ++ t).set i x h = if h' : i < s.size then s.set i x h' ++ t else s ++ t.set (i - s.size) x ⋯

Tactic:
rcases s with ⟨s⟩

Result:
case mk
α : Type u_1
t : Array α
i : Nat
x : α
s : List α
h : i < ({ toList := s } ++ t).size
⊢ ({ toList := s } ++ t).set i x h =
    if h' : i < { toList := s }.size then { toList := s }.set i x h' ++ t
    else { toList := s } ++ t.set (i - { toList := s }.size) x ⋯

Proof state:
case mk
α : Type u_1
t : Array α
i : Nat
x : α
s : List α
h : i < ({ toList := s } ++ t).size
⊢ ({ toList := s } ++ t).set i x h =
    if h' : i < { toList := s }.size then { toList := s }.set i x h' ++ t
    else { toList := s } ++ t.set (i - { toList := s }.size) x ⋯

Tactic:
rcases t with ⟨t⟩

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
h : i < ({ toList := s } ++ { toList := t }).size
⊢ ({ toList := s } ++ { toList := t }).set i x h =
    if h' : i < { toList := s }.size then { toList := s }.set i x h' ++ { toList := t }
    else { toList := s } ++ { toList := t }.set (i - { toList := s }.size) x ⋯

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : List α
h : i < ({ toList := s } ++ { toList := t }).size
⊢ (if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x).toArray =
    if h : i < { toList := s }.size then (s.set i x ++ t).toArray else (s ++ t.set (i - { toList := s }.size) x).toArray

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
theorem eLpNorm_le_eLpNorm_fderiv_one  {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
    {p : ℝ≥0} (hp : NNReal.IsConjExponent (finrank ℝ E) p) :
    eLpNorm u p μ ≤ eLpNormLESNormFDerivOneConst μ p * eLpNorm (fderiv ℝ u) 1 μ

Proof state:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).IsConjExponent p
h0p : 0 < ↑p
⊢ eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ

Tactic:
rw [eLpNorm_one_eq_lintegral_enorm,
  ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le,
  ← ENNReal.coe_rpow_of_nonneg _ h0p.le, eLpNormLESNormFDerivOneConst, ← NNReal.rpow_mul,
  eLpNorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',
  inv_mul_cancel₀ h0p.ne', NNReal.rpow_one]

Result:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).IsConjExponent p
h0p : 0 < ↑p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p ∂μ ≤ ↑(lintegralPowLePowLIntegralFDerivConst μ ↑p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p

Proof state:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).IsConjExponent p
⊢ eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ

Tactic:
have h0p : 0 < (p : ℝ) := hp.coe.symm.pos

Result:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).IsConjExponent p
h0p : 0 < ↑p
⊢ eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ

Proof state:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).IsConjExponent p
h0p : 0 < ↑p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p ∂μ ≤ ↑(lintegralPowLePowLIntegralFDerivConst μ ↑p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p

Tactic:
exact lintegral_pow_le_pow_lintegral_fderiv μ hu h2u hp.coe

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
/-- The range of the adjoint action homomorphism from a Lie algebra `L` to the Lie algebra of its
derivations is an ideal of the latter. -/
lemma ad_isIdealMorphism : (ad R L).IsIdealMorphism

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (x : LieDerivation R L L) (y : L), ∃ z, (ad R L) (x y) = (ad R L) z

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (ad R L).IsIdealMorphism

Tactic:
simp_rw [LieHom.isIdealMorphism_iff, lie_der_ad_eq_ad_der]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (x : LieDerivation R L L) (y : L), ∃ z, (ad R L) (x y) = (ad R L) z
-- Mathlib/Algebra/Order/Group/Indicator.lean
@[to_additive]
lemma mulIndicator_apply_le' (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) :
    mulIndicator s f a ≤ y

Proof state:
case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa [ha] using hg ha

Result:
no goals

Proof state:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∈ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa [ha] using hfg ha

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
⊢ s.mulIndicator f a ≤ y

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∈ s
⊢ s.mulIndicator f a ≤ y

case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_dualCoannihilator_eq {W : Subspace K V} :
    W.dualAnnihilator.dualCoannihilator = W

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∃ φ, φ (Submodule.Quotient.mk v) ≠ 0) → ∃ φ, (∀ w ∈ W, φ w = 0) ∧ φ v ≠ 0

Tactic:
refine fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ (φ ∘ₗ mkQ W) w = 0

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (¬∀ (φ : Dual K (V ⧸ W)), φ (Submodule.Quotient.mk v) = 0) → ¬∀ (φ : Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0

Tactic:
push_neg

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∃ φ, φ (Submodule.Quotient.mk v) ≠ 0) → ∃ φ, (∀ w ∈ W, φ w = 0) ∧ φ v ≠ 0

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∉ W → ¬∀ (φ : Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0

Tactic:
rw [← Quotient.mk_eq_zero W, ← Module.forall_dual_apply_eq_zero_iff K]

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (¬∀ (φ : Dual K (V ⧸ W)), φ (Submodule.Quotient.mk v) = 0) → ¬∀ (φ : Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∉ W → v ∉ (dualAnnihilator W).dualCoannihilator

Tactic:
simp only [mem_dualAnnihilator, mem_dualCoannihilator]

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∉ W → ¬∀ (φ : Dual K V), (∀ w ∈ W, φ w = 0) → φ v = 0

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ (φ ∘ₗ mkQ W) w = 0

Tactic:
rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
refine le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∉ W → v ∉ (dualAnnihilator W).dualCoannihilator
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : 0 ≤ x ^ y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs <;>
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ x ^ y

Tactic:
rw [rpow_def_of_nonneg hx]

Result:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
-- Mathlib/Data/Sign.lean
theorem range_eq {α} (f : SignType → α) : Set.range f = {f zero, f neg, f pos}

Proof state:
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
classical rw [← Fintype.coe_image_univ, univ_eq]

Result:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}

Proof state:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}

Tactic:
simp [Finset.coe_insert]

Result:
no goals

Proof state:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}

Tactic:
classical simp [Finset.coe_insert]

Result:
no goals

Proof state:
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
rw [← Fintype.coe_image_univ, univ_eq]

Result:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
-- Mathlib/Algebra/BigOperators/Ring/Nat.lean
lemma odd_sum_iff_odd_card_odd {s : Finset ι} (f : ι → ℕ) :
    Odd (∑ i ∈ s, f i) ↔ Odd (s.filter fun x ↦ Odd (f x)).card

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Odd (∑ i ∈ s, f i) ↔ Odd #(filter (fun x => Odd (f x)) s)

Tactic:
simp only [← Nat.not_even_iff_odd, even_sum_iff_even_card_odd]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_mk_eq_map_mk_of_rel {r : α → α → Prop} {s t : Multiset α} (hst : s.Rel r t) :
    s.map (Quot.mk r) = t.map (Quot.mk r) :=
  Rel.recOn hst rfl fun hab _hst ih => by simp [ih, Quot.sound hab]

Proof state:
α : Type u_1
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a✝ b✝ : α
as✝ bs✝ : Multiset α
hab : r a✝ b✝
_hst : Rel r as✝ bs✝
ih : map (Quot.mk r) as✝ = map (Quot.mk r) bs✝
⊢ map (Quot.mk r) (a✝ ::ₘ as✝) = map (Quot.mk r) (b✝ ::ₘ bs✝)

Tactic:
simp [ih, Quot.sound hab]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem pow_prime_eq_one_iff {σ : Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)] :
    σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
apply forall_congr'

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a : ℕ), a ∈ σ.cycleType → a ∣ p ↔ a ∈ σ.cycleType → a = p

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a : ℕ), a ∈ σ.cycleType → a ∣ p ↔ a ∈ σ.cycleType → a = p

Tactic:
exact fun c ↦ ⟨fun hc h ↦ Or.resolve_left (hp.elim.eq_one_or_self_of_dvd c (hc h))
     (Nat.ne_of_lt' (one_lt_of_mem_cycleType h)),
   fun hc h ↦ by rw [hc h]⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc : c ∈ σ.cycleType → c = p
h : c ∈ σ.cycleType
⊢ c ∣ p

Tactic:
rw [hc h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
lemma Scheme.toSpecΓ_preimage_basicOpen (X : Scheme.{u}) (r : Γ(X, ⊤)) :
    X.toSpecΓ ⁻¹ᵁ (PrimeSpectrum.basicOpen r) = X.basicOpen r

Proof state:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r)) =
    X.basicOpen r

Tactic:
congr

Result:
case e_f
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r

Proof state:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]

Result:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r)) =
    X.basicOpen r

Proof state:
case e_f
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).hom) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r

Tactic:
exact Iso.inv_hom_id_apply (C := CommRingCat) _ _

Result:
no goals

Proof state:
case e_f
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r

Tactic:
rw [Scheme.toSpecΓ_appTop]

Result:
case e_f
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).hom) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r
-- Mathlib/Data/List/TakeWhile.lean
theorem takeWhile_eq_nil_iff : takeWhile p l = [] ↔ ∀ hl : 0 < l.length, ¬p (l.get ⟨0, hl⟩)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true

Tactic:
induction' l with x xs IH

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p ([].get ⟨0, hl⟩) = true

case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
h : 0 < [].length
⊢ p ([].get ⟨0, h⟩) = false

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
by_cases hp : p x <;> simp [hp, IH]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p ([].get ⟨0, hl⟩) = true

Tactic:
simp only [takeWhile_nil, Bool.not_eq_true, true_iff]

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < [].length), p ([].get ⟨0, hl⟩) = false

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < [].length), p ([].get ⟨0, hl⟩) = false

Tactic:
intro h

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
h : 0 < [].length
⊢ p ([].get ⟨0, h⟩) = false
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem exp_of_re_eq_zero (q : Quaternion ℝ) (hq : q.re = 0) :
    exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

Proof state:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
simp_rw [← expSeries_apply_eq]

Result:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)

Proof state:
q : ℍ
hq : q.re = 0
⊢ exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
rw [exp_eq_tsum]

Result:
q : ℍ
hq : q.re = 0
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

Proof state:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
exact hasSum_expSeries_of_imaginary hq (Real.hasSum_cos _) (Real.hasSum_sin _)

Result:
no goals

Proof state:
q : ℍ
hq : q.re = 0
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
refine HasSum.tsum_eq ?_

Result:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)
-- Mathlib/Data/List/InsertIdx.lean
theorem get_insertIdx_of_lt (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk : k < l.length)
    (hk' : k < (insertIdx n x l).length := hk.trans_le (length_le_length_insertIdx _ _ _)) :
    (insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Proof state:
α : Type u
l : List α
x : α
n k : ℕ
hn : k < n
hk : k < l.length
hk' : optParam (k < (insertIdx n x l).length) ⋯
⊢ (insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Tactic:
simp_all [getElem_insertIdx_of_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem lt_of_mul_lt_mul_right {a b c : Nat} (h : b * a < c * a) : b < c

Proof state:
a b c : Nat
h : b * a < c * a
⊢ b < c

Tactic:
rw [Nat.mul_comm b a, Nat.mul_comm c a] at h

Result:
a b c : Nat
h : a * b < a * c
⊢ b < c

Proof state:
a b c : Nat
h : a * b < a * c
⊢ b < c

Tactic:
exact Nat.lt_of_mul_lt_mul_left h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem schur_complement_eq₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜)
    (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (x : m → 𝕜) (y : n → 𝕜) [Invertible D]
    (hD : D.IsHermitian) :
    (star (x ⊕ᵥ y)) ᵥ* (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
      (star ((D⁻¹ * Bᴴ) *ᵥ x + y)) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) +
        (star x) ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) =
    star ((D⁻¹ * Bᴴ) *ᵥ x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) + star x ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x

Tactic:
simp [Function.star_sumElim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hD.eq,
  conjTranspose_nonsing_inv, star_mulVec]

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝⁵ : CommRing 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)

Tactic:
abel

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma append_cast_right {n m} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ)
    (h : m' = m) :
    Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ (Fin.cast <| by rw [h])

Proof state:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ append xs (ys ∘ Fin.cast h) = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h

Result:
α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯

Proof state:
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
a : α
⊢ (map f l).headD (f a) = f (l.headD a)

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/Fintype/Order.lean
theorem Directed.finite_set_le (D : Directed r f) {s : Set γ} (hs : s.Finite) :
    ∃ z, ∀ i ∈ s, r (f i) (f z)

Proof state:
case h.e'_2.h.h.a
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)

Tactic:
rw [Set.Finite.mem_toFinset]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ z, ∀ i ∈ s, r (f i) (f z)

Tactic:
convert D.finset_le hs.toFinset using 3

Result:
case h.e'_2.h.h.a
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)