harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp]
lemma isFinitelySemisimple_sub_algebraMap_iff {μ : R} :
    (f - algebraMap R (End R M) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
p : Submodule R M
h : p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p
x : M
hx : x ∈ p
⊢ x ∈ Submodule.comap f p

Tactic:
simpa using p.add_mem (h hx) (p.smul_mem μ hx)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
  simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p

Tactic:
refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
p : Submodule R M
h : p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p
x : M
hx : x ∈ p
⊢ x ∈ Submodule.comap f p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem submonoid_closure (hpos : ∀ x : α, x ∈ s → 1 ≤ x) (h : s.IsPWO) :
    IsPWO (Submonoid.closure s : Set α)

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ ∀ a₁ ∈ {l | ∀ x ∈ l, x ∈ s},
    ∀ a₂ ∈ {l | ∀ x ∈ l, x ∈ s}, List.SublistForall₂ (fun x1 x2 => x1 ≤ x2) a₁ a₂ → a₁.prod ≤ a₂.prod

Tactic:
exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s)).IsPWO

Tactic:
rw [Submonoid.closure_eq_image_prod]

Result:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (List.prod '' {l | ∀ x ∈ l, x ∈ s}).IsPWO
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_iff_isSheaf_forget (s : A' ⥤ Type max v₁ u₁) [HasLimits A'] [PreservesLimits s]
    [s.ReflectsIsomorphisms] : IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A' : Type u₂
inst✝³ : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A'
inst✝¹ : PreservesLimits s
inst✝ : s.ReflectsIsomorphisms
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Tactic:
have : HasLimitsOfSize.{v₁, max v₁ u₁} A' := hasLimitsOfSizeShrink.{_, _, u₁, 0} A'

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A' : Type u₂
inst✝³ : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A'
inst✝¹ : PreservesLimits s
inst✝ : s.ReflectsIsomorphisms
this : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A' : Type u₂
inst✝³ : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A'
inst✝¹ : PreservesLimits s
inst✝ : s.ReflectsIsomorphisms
this✝ : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
this : PreservesLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, max u₁ v₁, u₂, max (u₁ + 1) (v₁ + 1)} s
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Tactic:
apply isSheaf_iff_isSheaf_comp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A' : Type u₂
inst✝³ : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A'
inst✝¹ : PreservesLimits s
inst✝ : s.ReflectsIsomorphisms
this : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)

Tactic:
have : PreservesLimitsOfSize.{v₁, max v₁ u₁} s := preservesLimitsOfSize_shrink.{_, 0, _, u₁} s

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A' : Type u₂
inst✝³ : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
s : A' ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A'
inst✝¹ : PreservesLimits s
inst✝ : s.ReflectsIsomorphisms
this✝ : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'
this : PreservesLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, max u₁ v₁, u₂, max (u₁ + 1) (v₁ + 1)} s
⊢ IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measurable_of_tendsto' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u]
    [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
    Measurable g

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Measurable fun x => ↑(g x)

Tactic:
refine ENNReal.measurable_of_tendsto' u hf ?_

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Tendsto (fun i x => ↑(f i x)) u (𝓝 fun x => ↑(g x))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ ∀ (x : α), Tendsto (fun i => ↑(f i x)) u (𝓝 ↑(g x))

Tactic:
exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ Measurable g

Tactic:
simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Measurable fun x => ↑(g x)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Tendsto (fun i x => ↑(f i x)) u (𝓝 fun x => ↑(g x))

Tactic:
rw [tendsto_pi_nhds] at lim ⊢

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ ∀ (x : α), Tendsto (fun i => ↑(f i x)) u (𝓝 ↑(g x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_flatMap {p : β → Prop} {l : Array α} {f : α → Array β} :
    (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b

Proof state:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
⊢ (∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b) → ∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x

Tactic:
intros

Result:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Proof state:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
⊢ (∀ (x : β), x ∈ flatMap f l → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
simp only [mem_flatMap, forall_exists_index, and_imp]

Result:
β : Type u_1
α : Type u_2
p : β → Prop
l : Array α
f : α → Array β
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
-- Mathlib/Data/PFun.lean
theorem dom_of_mem_fix {f : α →. β ⊕ α} {a : α} {b : β} (h : b ∈ f.fix a) : (f a).Dom

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ (f a).Dom

Tactic:
exact h₂.fst.fst

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ (f a).Dom

Tactic:
rw [WellFounded.fixFEq] at h₂

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ (f a).Dom

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ (f a).Dom

Tactic:
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ (f a).Dom
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_algebraMap (r : R) : algebraMap R (CliffordAlgebra Q) r⌊d = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
⊢ (contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0

Tactic:
rw [contractRight_eq, reverse.commutes, contractLeft_algebraMap, map_zero]

Result:
no goals
-- Mathlib/Order/Antichain.lean
theorem image_relEmbedding (hs : IsAntichain r s) (φ : r ↪r r') : IsAntichain r' (φ '' s)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Tactic:
rw [Set.mem_image] at hb hb'

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Tactic:
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
⊢ False

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a = φ a'

Tactic:
rw [haa']

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
⊢ False

Tactic:
exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (⇑φ '' s)

Tactic:
intro b hb b' hb' h₁ h₂

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
    (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)

Proof state:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else false)

Tactic:
rw [signExtend_eq_setWidth_of_msb_false hmsb]

Result:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (setWidth v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else false)

Proof state:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (setWidth v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else false)

Tactic:
by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v i : Nat
⊢ (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)

Tactic:
rcases hmsb : x.msb with rfl | rfl

Result:
case false
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = false
⊢ (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else false)

case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else true)

Proof state:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else true)

Tactic:
rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]

Result:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (~~~setWidth v (~~~x)).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else true)

Proof state:
case true
w : Nat
x : BitVec w
v i : Nat
hmsb : x.msb = true
⊢ (~~~setWidth v (~~~x)).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else true)

Tactic:
by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_eq_natDegree (hp : p ≠ 0) : degree p = (natDegree p : WithBot ℕ)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = Option.some n
⊢ p.degree = ↑p.natDegree

Tactic:
rw [natDegree, hn]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = Option.some n
⊢ Option.some n = ↑(WithBot.unbotD 0 (Option.some n))

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = ↑p.natDegree

Tactic:
have hn : degree p = some n := Classical.not_not.1 hn

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = Option.some n
⊢ p.degree = ↑p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.degree = ↑p.natDegree

Tactic:
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = ↑p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = Option.some n
⊢ Option.some n = ↑(WithBot.unbotD 0 (Option.some n))

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = ℝ ∙ y) :
    (2 : ℤ) • o.oangle x z = (2 : ℤ) • o.oangle y z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : ∃ z, z • x = y
⊢ 2 • o.oangle x z = 2 • o.oangle y z

Tactic:
rcases h with ⟨r, rfl⟩

Result:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
r : ℝˣ
⊢ 2 • o.oangle x z = 2 • o.oangle (r • x) z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : Submodule.span ℝ {x} = Submodule.span ℝ {y}
⊢ 2 • o.oangle x z = 2 • o.oangle y z

Tactic:
rw [Submodule.span_singleton_eq_span_singleton] at h

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : ∃ z, z • x = y
⊢ 2 • o.oangle x z = 2 • o.oangle y z

Proof state:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
r : ℝˣ
⊢ 2 • o.oangle x z = 2 • o.oangle (r • x) z

Tactic:
exact (o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem divisors_one : divisors 1 = {1}

Proof state:
case h
a✝ : ℕ
⊢ a✝ ∈ divisors 1 ↔ a✝ ∈ {1}

Tactic:
simp

Result:
no goals

Proof state:
⊢ divisors 1 = {1}

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ a✝ ∈ divisors 1 ↔ a✝ ∈ {1}
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ≥0) (hw' : ∑ i ∈ s, w i = 1) :
    (∏ i ∈ s, z i ^ (w i : ℝ)) ≤ ∑ i ∈ s, w i * z i :=
  mod_cast
    Real.geom_mean_le_arith_mean_weighted _ _ _ (fun i _ => (w i).coe_nonneg)
      (by assumption_mod_cast) fun i _ => (z i).coe_nonneg

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, ↑(w i) = 1

Tactic:
assumption_mod_cast

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination :
    (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential.comp
        (Finsupp.linearCombination S (KaehlerDifferential.D R S)) =
      Submodule.mkQ _

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a

Tactic:
conv_rhs => rw [← Finsupp.smul_single_one a b, LinearMap.map_smul]

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b • 1𝖣a

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S) = (kerTotal R S).mkQ

Tactic:
apply Finsupp.lhom_ext

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ (a b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b • 1𝖣a

Tactic:
simp [KaehlerDifferential.derivationQuotKerTotal_apply]

Result:
no goals

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ (a b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a

Tactic:
intro a b

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
@[simp]
lemma extendMap_id : extendMap (𝟙 K) e = 𝟙 _

Proof state:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Tactic:
simp [extendMap_f _ e hi]

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
⊢ extendMap (𝟙 K) e = 𝟙 (K.extend e)

Tactic:
ext i'

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'

Tactic:
obtain ⟨i, hi⟩ := hi'

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = (𝟙 (K.extend e)).f i'