harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_C_mul_X_sub_C_pow {x y : F} {n : ℕ} (hx : x ≠ 0) :
    (C x * (X - C y) ^ n).natSepDegree = if n = 0 then 0 else 1

Proof state:
F : Type u
inst✝ : Field F
x y : F
n : ℕ
hx : x ≠ 0
⊢ (C x * (X - C y) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_C_mul _ hx, natSepDegree_X_sub_C_pow]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma rootSpace_neg_nsmul_add_chainTop_of_le {n : ℕ} (hn : n ≤ chainLength α β) :
    rootSpace H (- (n • α) + chainTop α β) ≠ ⊥

Proof state:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥

Tactic:
obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero

Result:
case neg.intro.intro
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥

Proof state:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
hα : α.IsZero
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥

Tactic:
simpa only [hα.eq, smul_zero, neg_zero, chainTop_zero, zero_add, ne_eq] using β.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs

Proof state:
α : Type u_1
as bs : Array α
start : Nat
⊢ (if hlt : start < as.size then
      match 0 with
      | 0 => bs
      | i'.succ => extract.loop as i' (start + 1) (bs.push (as.get start hlt))
    else bs) =
    bs

Tactic:
split <;> rfl

Result:
no goals

Proof state:
α : Type u_1
as bs : Array α
start : Nat
⊢ extract.loop as 0 start bs = bs

Tactic:
rw [extract.loop]

Result:
α : Type u_1
as bs : Array α
start : Nat
⊢ (if hlt : start < as.size then
      match 0 with
      | 0 => bs
      | i'.succ => extract.loop as i' (start + 1) (bs.push (as.get start hlt))
    else bs) =
    bs
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem map_gcd [CommGroupWithZero R] {f : ArithmeticFunction R}
    (hf : f.IsMultiplicative) {x y : ℕ} (hf_lcm : f (x.lcm y) ≠ 0) :
    f (x.gcd y) = f x * f y / f (x.lcm y)

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : f (x.lcm y) ≠ 0
⊢ f (x.gcd y) = f x * f y / f (x.lcm y)

Tactic:
rw [←hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot]
    {F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) :
    UniformContinuous f

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f

Tactic:
rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun i => F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun i => F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Tactic:
exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem degree_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
    (finSuccEquiv R n f).degree = degreeOf 0 f

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.172834} {β : Type ?u.172837} (f : α → β), (fun x => x) ∘ f = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.172834} {β : Type ?u.172837} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.172902} {β : Type ?u.172905} (f : α → β), (f ∘ fun x => x) = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.172834} {β : Type ?u.172837} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.172902} {β : Type ?u.172905} (f : α → β), (f ∘ fun x => x) = f
⊢ (((finSuccEquiv R n) f).support.sup fun x => x) = degreeOf 0 f

Tactic:
rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.172834} {β : Type ?u.172837} (f : α → β), (fun x => x) ∘ f = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.172834} {β : Type ?u.172837} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.172902} {β : Type ?u.172905} (f : α → β), (f ∘ fun x => x) = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
  rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.172902} {β : Type ?u.172905} (f : α → β), (f ∘ fun x => x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x => x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.172902} {β : Type ?u.172905} (f : α → β), (f ∘ fun x => x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x => x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
rw [Polynomial.degree, ← h', Nat.cast_withBot,
  Finset.coe_sup_of_nonempty (support_finSuccEquiv_nonempty h), Finset.max_eq_sup_coe, h₁]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
lemma exists_eventually_atTop {r : α → β → Prop} :
    (∃ b, ∀ᶠ a in atTop, r a b) ↔ ∀ᶠ a₀ in atTop, ∃ b, ∀ a ≥ a₀, r a b

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ x y, ∀ b ≥ x, r b y) ↔ ∃ a, ∀ b ≥ a, ∃ b_1, ∀ a ≥ b, r a b_1

Tactic:
exact exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦
  H n (hb.trans hn)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b, ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ b, ∀ a ≥ a₀, r a b

Tactic:
simp_rw [eventually_atTop, ← exists_swap (α := α)]

Result:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ x y, ∀ b ≥ x, r b y) ↔ ∃ a, ∀ b ≥ a, ∃ b_1, ∀ a ≥ b, r a b_1
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
@[simp] lemma locallyLipschitzOn_univ : LocallyLipschitzOn univ f ↔ LocallyLipschitz f

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ LocallyLipschitzOn univ f ↔ LocallyLipschitz f

Tactic:
simp [LocallyLipschitzOn, LocallyLipschitz]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsSigmaCompact.isLindelof (hs : IsSigmaCompact s) :
    IsLindelof s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsSigmaCompact s
⊢ IsLindelof s

Tactic:
rw [IsSigmaCompact] at hs

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = s
⊢ IsLindelof s

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
hl : ∀ (n : ℕ), IsLindelof (K n)
⊢ IsLindelof (⋃ n, K n)

Tactic:
exact isLindelof_iUnion hl

Result:
no goals

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
⊢ IsLindelof s

Tactic:
rw [← huniv]

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
⊢ IsLindelof (⋃ n, K n)

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
⊢ IsLindelof (⋃ n, K n)

Tactic:
have hl : ∀ n, IsLindelof (K n) := fun n ↦ IsCompact.isLindelof (hc n)

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
hl : ∀ (n : ℕ), IsLindelof (K n)
⊢ IsLindelof (⋃ n, K n)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = s
⊢ IsLindelof s

Tactic:
rcases hs with ⟨K, ⟨hc, huniv⟩⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
K : ℕ → Set X
hc : ∀ (n : ℕ), IsCompact (K n)
huniv : ⋃ n, K n = s
⊢ IsLindelof s
-- Mathlib/Order/SupIndep.lean
theorem sSupIndep_pair {a b : α} (hab : a ≠ b) :
    sSupIndep ({a, b} : Set α) ↔ Disjoint a b

Proof state:
case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
convert h.symm using 1

Result:
case h.e'_5
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a

Proof state:
case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} → Disjoint a b

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
h : sSupIndep {a, b}
⊢ Disjoint a b

Proof state:
case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
h : sSupIndep {a, b}
⊢ Disjoint a b

Tactic:
exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} ↔ Disjoint a b

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} → Disjoint a b

case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Proof state:
case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Tactic:
rintro h c ((rfl : c = a) | (rfl : c = b))

Result:
case mpr.inl
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))

case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Proof state:
case mpr.inl
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))

Tactic:
convert h using 1

Result:
case h.e'_5
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b

Proof state:
case h.e'_5
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b

Tactic:
simp [hab, sSup_singleton]

Result:
no goals

Proof state:
case h.e'_5
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a

Tactic:
simp [hab, sSup_singleton]

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem smul_polynomial (m : M) (p : Polynomial (FixedPoints.subfield M F)) : m • p = p :=
  Polynomial.induction_on p (fun x => by rw [Polynomial.smul_C, smul])
    (fun p q ihp ihq => by rw [smul_add, ihp, ihq]) fun n x _ => by
    rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]

Proof state:
M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p✝ p q : Polynomial ↥(subfield M F)
ihp : m • p = p
ihq : m • q = q
⊢ m • (p + q) = p + q

Tactic:
rw [smul_add, ihp, ihq]

Result:
no goals

Proof state:
M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
x : ↥(subfield M F)
⊢ m • Polynomial.C x = Polynomial.C x

Tactic:
rw [Polynomial.smul_C, smul]

Result:
no goals

Proof state:
M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n
⊢ m • (Polynomial.C x * Polynomial.X ^ (n + 1)) = Polynomial.C x * Polynomial.X ^ (n + 1)

Tactic:
rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevInTwo_fst (l : { l : List α // l.length = n }) :
    (splitRevInTwo l).1 = ⟨(splitInTwo l).1.1.reverse, by simp; omega⟩

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitRevInTwo l).fst = ⟨(splitInTwo l).fst.val.reverse, ⋯⟩

Tactic:
simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_fst]

Result:
no goals

Proof state:
α : Type ?u.44149
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo l).fst.val.reverse.length = (n + 1) / 2

Tactic:
simp

Result:
α : Type ?u.44149
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) l.val.length = (n + 1) / 2

Proof state:
α : Type ?u.44149
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) l.val.length = (n + 1) / 2

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem IsGLB.biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) :
    ⋃ x ∈ s, Ici x = Ici a

Proof state:
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ x ∈ s, Ici x = Ici a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Result:
case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ i ∈ s, Ici i

Proof state:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

Result:
no goals

Proof state:
case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

Tactic:
exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
/-- Any morphism between initial objects is an isomorphism. -/
lemma isIso_of_isInitial {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) :
    IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X

Tactic:
apply IsInitial.hom_ext hX

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y

Tactic:
simp only [IsInitial.to_comp, IsInitial.to_self, and_true]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
refine ⟨⟨IsInitial.to hY X, ?_⟩⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).1.isEmpty = false

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).val.isEmpty = false

Tactic:
simp_to_model [insert] using List.isEmpty_insertEntry

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_map_complex (f : E ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : E) :
    ω x y = (conj (f x) * f y).im

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.areaForm x) y = (o.areaForm x) (f.symm (f y))

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.areaForm x) y = (o.areaForm (f.symm (f x))) (f.symm (f y))

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im

Tactic:
rw [← Complex.areaForm, ← hf, areaForm_map (hF := _)]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ (o.areaForm x) y = (o.areaForm (f.symm (f x))) (f.symm (f y))
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem inits_eq_initsTR : @inits = @initsTR

Proof state:
case h.h
α : Type u_1
l : List α
⊢ l.inits = (foldr (fun a arrs => (Array.map (fun t => a :: t) arrs).push []) #[[]] l).toList.reverse

Tactic:
induction l <;> simp [*, map_reverse]

Result:
no goals

Proof state:
case h.h
α : Type u_1
l : List α
⊢ l.inits = l.initsTR

Tactic:
simp [initsTR]

Result:
case h.h
α : Type u_1
l : List α
⊢ l.inits = (foldr (fun a arrs => (Array.map (fun t => a :: t) arrs).push []) #[[]] l).toList.reverse

Proof state:
⊢ @inits = @initsTR

Tactic:
funext α l

Result:
case h.h
α : Type u_1
l : List α
⊢ l.inits = l.initsTR
-- Mathlib/Data/Multiset/Nodup.lean
theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) :
    a ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
  ⟨fun h =>
    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' => by
      refine count_eq_zero.1 ?_ h
      rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
      exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t

Tactic:
exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0

Tactic:
rw [count_sub a s t, Nat.sub_eq_zero_iff_le]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ False

Tactic:
refine count_eq_zero.1 ?_ h

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem locallyConvexSpace_iInf {ts' : ι → TopologicalSpace E}
    (h' : ∀ i, @LocallyConvexSpace 𝕜 E _ _ _ (ts' i)) :
    @LocallyConvexSpace 𝕜 E _ _ _ (⨅ i, ts' i)

Proof state:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ ∀ t ∈ range fun i => ts' i, LocallyConvexSpace 𝕜 E

Tactic:
rwa [forall_mem_range]

Result:
no goals

Proof state:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine locallyConvexSpace_sInf ?_

Result:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ ∀ t ∈ range fun i => ts' i, LocallyConvexSpace 𝕜 E
-- Mathlib/LinearAlgebra/Pi.lean
theorem single_eq_pi_diag (i : ι) : single R φ i = pi (diag i)

Proof state:
case h.e'_2.h.e'_1
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = id x

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ (single R φ i) x j = (pi (diag i)) x j

Tactic:
convert (update_apply 0 x i j _).symm

Result:
case h.e'_2.h.e'_1
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = id x

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
⊢ single R φ i = pi (diag i)

Tactic:
ext x j

Result:
case h.h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ (single R φ i) x j = (pi (diag i)) x j