harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem mlieBracketWithin_congr_set' (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬x = ↑(extChartAt I x).symm z

Tactic:
rw [(extChartAt I x).eq_symm_apply (by simp) hz.2]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬↑(extChartAt I x) x = z
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.units_lineMap {p : ι → P} (hp : AffineIndependent k p) (j : ι)
    (w : ι → Units k) : AffineIndependent k fun i => AffineMap.lineMap (p j) (p i) (w i : k)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => (AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ (AffineMap.lineMap (p j) (p j)) ↑(w j)

Tactic:
simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(w ↑i) • (p ↑i -ᵥ p j)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
hp : AffineIndependent k p
j : ι
w : ι → kˣ
⊢ AffineIndependent k fun i => (AffineMap.lineMap (p j) (p i)) ↑(w i)

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp ⊢

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => (AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ (AffineMap.lineMap (p j) (p j)) ↑(w j)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
j : ι
hp : LinearIndependent k fun i => p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i => ↑(w ↑i) • (p ↑i -ᵥ p j)

Tactic:
exact hp.units_smul fun i => w i

Result:
no goals
-- Mathlib/RingTheory/HopfAlgebra/Basic.lean
@[simp]
lemma sum_mul_antipode_eq {a : A} (repr : Repr R a) :
    ∑ i ∈ repr.index, repr.left i * antipode (R := R) (repr.right i) =
      algebraMap R A (counit a)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a
⊢ ∑ i ∈ repr.index, repr.left i * antipode (repr.right i) = (algebraMap R A) (counit a)

Tactic:
simpa [← repr.eq, map_sum] using congr($(mul_antipode_lTensor_comul (R := R)) a)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.mono (hf : IsRatCondKernelCDFAux f κ ν) (a : α) :
    ∀ᵐ c ∂(ν a), Monotone (f (a, c))

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))

Tactic:
unfold Monotone

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a_1 : β) ∂ν a, f (a, a_1) i ≤ f (a, a_1) i_1

Tactic:
exact fun _ _ hqr ↦ hf.mono' a hqr

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b

Tactic:
simp_rw [ae_all_iff]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a_1 : β) ∂ν a, f (a, a_1) i ≤ f (a, a_1) i_1
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem eLpNorm_le_seminorm (p : ℝ≥0∞) (μ : Measure E

Proof state:
case bc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ k • f x) ⊤ μ ≤
    2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)

Result:
case bc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖₊ ≤ ↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ * 2 ^ k *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_modifyKey (k : α) (f : β → β) (l : List ((_ : α) × β)) :
    (modifyKey k f l).length = l.length

Proof state:
case cons
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
next ih =>
simp only [modifyKey]
split <;> next h => simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
ih : (modifyKey k f tail✝).length = tail✝.length
x✝ : Option β
v✝ : β
h : getValue? k (head✝ :: tail✝) = some v✝
⊢ (replaceEntry k (f v✝) (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (match getValue? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)).length =
    (head✝ :: tail✝).length

Tactic:
split <;> next h => simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
⊢ (modifyKey k f []).length = [].length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
simp only [modifyKey]

Result:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (match getValue? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)).length =
    (head✝ :: tail✝).length

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (modifyKey k f l).length = l.length

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
⊢ (modifyKey k f []).length = [].length

case cons
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_eq_same {i b} : (single i b : Π₀ i, β i) i = b

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
⊢ (single i b) i = b

Tactic:
simp only [single_apply, dite_eq_ite, ite_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem bind_map_left [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) :
    ((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a))

Proof state:
m : Type u_1 → Type u_2
α β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m α
g : β → m γ
⊢ (do
      let b ←
        do
          let a ← x
          pure (f a)
      g b) =
    do
    let a ← x
    g (f a)

Tactic:
simp only [bind_assoc, pure_bind]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m α
g : β → m γ
⊢ (do
      let b ← f <$> x
      g b) =
    do
    let a ← x
    g (f a)

Tactic:
rw [← bind_pure_comp]

Result:
m : Type u_1 → Type u_2
α β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m α
g : β → m γ
⊢ (do
      let b ←
        do
          let a ← x
          pure (f a)
      g b) =
    do
    let a ← x
    g (f a)
-- Mathlib/CategoryTheory/Bicategory/Coherence.lean
theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
    (preinclusion B).map ⟨p⟩ ◁ η ≫ (normalizeIso p g).hom =
      (normalizeIso p f).hom ≫
        (preinclusion B).map₂ (eqToHom (Discrete.ext (normalizeAux_congr p η)))

Proof state:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))

Result:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
this : (normalizeIso (normalizeAux p f✝) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g✝) h).hom ≫ eqToHom ⋯
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      (preinclusion B).map₂ (eqToHom ⋯)
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem two_le_chromaticNumber_of_adj {α} {G : SimpleGraph α} {u v : α} (hadj : G.Adj u v) :
    2 ≤ G.chromaticNumber

Proof state:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
⊢ False

Tactic:
have hc : G.Colorable 1 := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)

Result:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
hc : G.Colorable 1
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
⊢ 2 ≤ G.chromaticNumber

Tactic:
refine le_of_not_lt ?_

Result:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
⊢ ¬G.chromaticNumber < 2

Proof state:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
⊢ ¬G.chromaticNumber < 2

Tactic:
intro h

Result:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
hc : G.Colorable 1
c : G.Coloring (Fin 1) := Nonempty.some hc
⊢ False

Tactic:
exact c.valid hadj (Subsingleton.elim (c u) (c v))

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
hc : G.Colorable 1
⊢ False

Tactic:
let c : G.Coloring (Fin 1) := hc.some

Result:
α : Type u_1
G : SimpleGraph α
u v : α
hadj : G.Adj u v
h : G.chromaticNumber < 2
hc : G.Colorable 1
c : G.Coloring (Fin 1) := Nonempty.some hc
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
    (x.sshiftRight s)[i] = (if s + i < w then x.getLsbD (s + i) else x.msb)

Proof state:
w : Nat
x : BitVec w
s i : Nat
h : i < w
⊢ (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else x.msb

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

Result:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
⊢ (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else false

case true
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = true
⊢ (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else true

Proof state:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
hlsb : x.getLsbD (s + i) = true
⊢ s + i < w

Tactic:
apply BitVec.lt_of_getLsbD hlsb

Result:
no goals

Proof state:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
⊢ (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else false

Tactic:
simp only [sshiftRight_eq_of_msb_false hmsb, getElem_ushiftRight, Bool.if_false_right,
Bool.iff_and_self, decide_eq_true_eq]

Result:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
⊢ x.getLsbD (s + i) = true → s + i < w

Proof state:
case true
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = true
⊢ (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else true

Tactic:
simp [sshiftRight_eq_of_msb_true hmsb]

Result:
no goals

Proof state:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
⊢ x.getLsbD (s + i) = true → s + i < w

Tactic:
intros hlsb

Result:
case false
w : Nat
x : BitVec w
s i : Nat
h : i < w
hmsb : x.msb = false
hlsb : x.getLsbD (s + i) = true
⊢ s + i < w
-- Mathlib/RingTheory/Norm/Basic.lean
lemma norm_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [Ring C]
    [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C)
    (x : C) :
    e (Algebra.norm A x) = Algebra.norm B x

Proof state:
case pos.intro.intro
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
⊢ e ((norm A) x) = (norm B) x

Tactic:
letI : Algebra A B := RingHom.toAlgebra e

Result:
case pos.intro.intro
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this : Algebra A B := (↑e).toAlgebra
⊢ e ((norm A) x) = (norm B) x

Proof state:
case pos.intro.intro.e_M
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e.mapMatrix ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x) = (leftMulMatrix b) x

Tactic:
ext i j

Result:
case pos.intro.intro.e_M.a
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis { x // x ∈ s } B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
i j : { x // x ∈ s }
⊢ e.mapMatrix ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x) i j = (leftMulMatrix b) x i j
-- Mathlib/Data/Fintype/Order.lean
theorem Finite.bddAbove_range [IsDirected α (· ≤ ·)] (f : β → α) : BddAbove (Set.range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
⊢ BddAbove (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_le f

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)

Tactic:
refine ⟨M, fun a ha => ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M

Tactic:
obtain ⟨b, rfl⟩ := ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M

Tactic:
exact hM b

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_one (k : ℕ) : multichoose (1 : R) k = 1

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

Tactic:
rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
  multichoose_zero_succ, zero_add, zero_add, ih]

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ multichoose 1 0 = 1

Tactic:
exact multichoose_zero_right 1

Result:
no goals

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ multichoose 1 k = 1

Tactic:
induction k with
| zero => exact multichoose_zero_right 1
| succ n ih =>
  rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
    multichoose_zero_succ, zero_add, zero_add, ih]

Result:
no goals

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ 1 = 0 + 1

Tactic:
exact (@zero_add R _ 1).symm

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n]
    {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
    σ ∈ (sumCongrHom m n).range

Proof state:
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x

Tactic:
rintro x ⟨a, ha⟩

Result:
case intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ ∃ a, Sum.inl a = σ x

Proof state:
case intro.a
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ Sum.inr b ∈ Set.range Sum.inr

Tactic:
exact ⟨b, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittAdd_zero : wittAdd p 0 = X (0, 0) + X (1, 0)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittAdd p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))

Tactic:
simp only [wittAdd, wittStructureRat, map_add, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittAdd p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))