harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma disjoint_rootSpan_ker_rootForm :
    Disjoint P.rootSpan (LinearMap.ker P.RootForm)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint P.rootSpan (LinearMap.ker P.RootForm)

Tactic:
rw [← P.ker_polarization_eq_ker_rootForm]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint P.rootSpan (LinearMap.ker P.Polarization)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint P.rootSpan (LinearMap.ker P.Polarization)

Tactic:
refine Submodule.disjoint_ker_of_finrank_le (L := P.rootSpan) P.Polarization ?_

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ finrank R ↥P.rootSpan ≤ finrank R ↥(Submodule.map P.Polarization P.rootSpan)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ finrank R ↥P.rootSpan ≤ finrank R ↥(Submodule.map P.Polarization P.rootSpan)

Tactic:
rw [P.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, P.finrank_corootSpan_eq]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ Disjoint P.rootSpan (LinearMap.ker P.RootForm)

Tactic:
have : IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint P.rootSpan (LinearMap.ker P.RootForm)
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
lemma infEdist_biUnion {ι : Type*} (f : ι → Set α) (I : Set ι) (x : α) :
    infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Type u_2
f : ι → Set α
I : Set ι
x : α
⊢ infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i)

Tactic:
simp only [infEdist_iUnion]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_coe_div_two (θ : ℝ) : (2 : ℤ) • (↑(θ / 2) : Angle) = θ

Proof state:
θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ

Tactic:
rw [← coe_zsmul, two_zsmul, add_halves]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma sdiff_edge {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Adj u v
⊢ G \ edge u v = G

Tactic:
simp [disjoint_edge, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w

Proof state:
case mk
α : Type u_1
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray = w.toArray ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = w

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.toArray =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.toArray =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v w : Vector α n
⊢ v.toArray = w.toArray ↔ v = w

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray = w.toArray ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = w
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_neg_add (n : ℕ) : ∀ k : ℕ,
    smeval (ascPochhammer ℕ (n + k + 1)) (-n : ℤ) = 0
  | 0 => by
    rw [add_zero, smeval_ascPochhammer_succ_neg]
  | k + 1 => by
    rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
      zero_mul]

Proof state:
n : ℕ
⊢ (ascPochhammer ℕ (n + 0 + 1)).smeval (-↑n) = 0

Tactic:
rw [add_zero, smeval_ascPochhammer_succ_neg]

Result:
no goals

Proof state:
n k : ℕ
⊢ (ascPochhammer ℕ (n + (k + 1) + 1)).smeval (-↑n) = 0

Tactic:
rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
  zero_mul]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
/-- `take_concat_get` in simp normal form -/
lemma take_concat_get' (l : List α) (i : ℕ) (h : i < l.length) :
  l.take i ++ [l[i]] = l.take (i + 1)

Proof state:
α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ take i l ++ [l[i]] = take (i + 1) l

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem npow_mul_assoc (k m n : ℕ) (x : M) :
    (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n)

Proof state:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
k m n : ℕ
x : M
⊢ x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

Tactic:
simp only [← npow_add, add_assoc]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem exists_eq_iff_rel (f : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' = b ∧ r a' a :=
  ⟨fun h => by
    rcases f.mem_range_of_rel h with ⟨a', rfl⟩
    exact ⟨a', rfl, f.map_rel_iff.1 h⟩,
    fun ⟨_, e, h⟩ => e ▸ f.map_rel_iff.2 h⟩

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b (f a)
⊢ ∃ a', f a' = b ∧ r a' a

Tactic:
rcases f.mem_range_of_rel h with ⟨a', rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a a' : α
h : s (f a') (f a)
⊢ ∃ a'_1, f a'_1 = f a' ∧ r a'_1 a

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a a' : α
h : s (f a') (f a)
⊢ ∃ a'_1, f a'_1 = f a' ∧ r a'_1 a

Tactic:
exact ⟨a', rfl, f.map_rel_iff.1 h⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.transpose_circulant : ∀ {n} (v : Fin n → α), (circulant v)ᵀ = circulant fun i => v (-i)
  | 0 => by simp [Injective, eq_iff_true_of_subsingleton]
  | _ + 1 => Matrix.transpose_circulant

Proof state:
α : Type u_1
⊢ ∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun i => v (-i)

Tactic:
simp [Injective, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem _root_.Function.Surjective.preValuationRing {R S : Type*} [Mul R] [PreValuationRing R]
    [Mul S] (f : R →ₙ* S) (hf : Function.Surjective f) :
    PreValuationRing S :=
  ⟨fun a b => by
    obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b
    obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
    exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]⟩

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a b : R
⊢ ∃ c, f a * c = f b ∨ f b * c = f a

Tactic:
obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b

Result:
case intro.intro.intro.inl
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a c : R
⊢ ∃ c_1, f a * c_1 = f (a * c) ∨ f (a * c) * c_1 = f a

case intro.intro.intro.inr
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
b c : R
⊢ ∃ c_1, f (b * c) * c_1 = f b ∨ f b * c_1 = f (b * c)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a b : S
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a b : R
⊢ ∃ c, f a * c = f b ∨ f b * c = f a

Proof state:
case intro.intro.intro.inl
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a c : R
⊢ ∃ c_1, f a * c_1 = f (a * c) ∨ f (a * c) * c_1 = f a

case intro.intro.intro.inr
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
b c : R
⊢ ∃ c_1, f (b * c) * c_1 = f b ∨ f b * c_1 = f (b * c)

Tactic:
exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Free.lean
theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃]
    [StrongRankCondition R] :
    Module.rank R S.X₂ = Module.rank R S.X₁ + Module.rank R S.X₃

Proof state:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
  Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]

Result:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Nonempty (Free.ChooseBasisIndex R ↑S.X₂ ≃ Free.ChooseBasisIndex R ↑S.X₁ ⊕ Free.ChooseBasisIndex R ↑S.X₃)

Proof state:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
haveI := free_shortExact hS'

Result:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Proof state:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Nonempty (Free.ChooseBasisIndex R ↑S.X₂ ≃ Free.ChooseBasisIndex R ↑S.X₁ ⊕ Free.ChooseBasisIndex R ↑S.X₃)

Tactic:
exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
  (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
lemma AffineSubspace.mem_of_wbtw {s : AffineSubspace R P} {x y z : P} (hxyz : Wbtw R x y z)
    (hx : x ∈ s) (hz : z ∈ s) : y ∈ s

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ (lineMap x z) ε ∈ s

Tactic:
exact lineMap_mem _ hx hz

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
hxyz : Wbtw R x y z
hx : x ∈ s
hz : z ∈ s
⊢ y ∈ s

Tactic:
obtain ⟨ε, -, rfl⟩ := hxyz

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ (lineMap x z) ε ∈ s
-- Mathlib/RingTheory/LaurentSeries.lean
theorem single_inv (d : ℤ) {α : F} (hα : α ≠ 0) :
    single (-d) (α⁻¹ : F) = (single (d : ℤ) (α : F))⁻¹

Proof state:
case h
F : Type u
inst✝ : Field F
d : ℤ
α : F
hα : α ≠ 0
⊢ (single d) α * (single (-d)) α⁻¹ = 1

Tactic:
simp [hα]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
d : ℤ
α : F
hα : α ≠ 0
⊢ (single (-d)) α⁻¹ = ((single d) α)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_right

Result:
case h
F : Type u
inst✝ : Field F
d : ℤ
α : F
hα : α ≠ 0
⊢ (single d) α * (single (-d)) α⁻¹ = 1
-- Mathlib/Analysis/Normed/MulAction.lean
theorem norm_smul (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖

Tactic:
apply norm_smul_le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
by_cases h : r = 0

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
simp [h, zero_smul α x]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖

Tactic:
rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
refine le_antisymm (norm_smul_le r x) ?_

Result:
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖

Tactic:
rw [inv_smul_smul₀ h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)

Tactic:
gcongr

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖

Tactic:
calc
  ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
  _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
  _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_mkArray_of_pos (w : stop = n) (h : p a) :
    (mkArray n a).filter p 0 stop = mkArray n a

Proof state:
stop n : Nat
α✝ : Type u_1
p : α✝ → Bool
a : α✝
w : stop = n
h : p a = true
⊢ filter p (mkArray n a) 0 stop = mkArray n a

Tactic:
simp [filter_mkArray, h, w]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_dite {P : Prop} [Decidable P]
    (X : C) {Y Z : C} (f : P → (Y ⟶ Z)) (f' : ¬P → (Y ⟶ Z)) :
      X ◁ (if h : P then f h else f' h) = if h : P then X ◁ f h else X ◁ f' h

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
⊢ (X ◁ if h : P then f h else f' h) = if h : P then X ◁ f h else X ◁ f' h

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_add (x y : BitVec w) (h : i ≤ w) :
    (x + y).setWidth i = x.setWidth i + y.setWidth i

Proof state:
w i : Nat
x y : BitVec w
h : i ≤ w
⊢ setWidth i (x + y) = setWidth i x + setWidth i y

Tactic:
have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h

Result:
w i : Nat
x y : BitVec w
h : i ≤ w
dvd : 2 ^ i ∣ 2 ^ w
⊢ setWidth i (x + y) = setWidth i x + setWidth i y

Proof state:
w i : Nat
x y : BitVec w
h : i ≤ w
dvd : 2 ^ i ∣ 2 ^ w
⊢ setWidth i (x + y) = setWidth i x + setWidth i y

Tactic:
simp [bv_toNat, h, Nat.mod_mod_of_dvd _ dvd]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem map_comp_inl : (map fn fg h).comp inl = inl.comp fn

Proof state:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
⊢ (map fn fg h).comp inl = inl.comp fn

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ rexp x

Tactic:
linarith [add_one_le_exp_of_nonneg hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_cons_of_pos {p : α → Bool} {a : α} {l : List α} (h : p a) :
    (a :: l).takeWhile p = a :: l.takeWhile p

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
h : p a = true
⊢ takeWhile p (a :: l) = a :: takeWhile p l

Tactic:
simp [takeWhile_cons, h]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem embDomain_injective (f : α ↪ β) : Function.Injective (embDomain f : (α →₀ M) → β →₀ M) :=
  fun l₁ l₂ h => ext fun a => by simpa only [embDomain_apply] using DFunLike.ext_iff.1 h (f a)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ l₁ a = l₂ a

Tactic:
simpa only [embDomain_apply] using DFunLike.ext_iff.1 h (f a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m)

Proof state:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
h' : i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp [h']

Result:
no goals

Proof state:
case neg
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
h' : ¬i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp_all [h']

Result:
no goals

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
by_cases h' : i < m

Result:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
h' : i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

case neg
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
h' : ¬i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
⊢ (x ++ y)[i] = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']

Result:
n m i : Nat
x : BitVec n
y : BitVec m
h : i < n + m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap_congr {f g : α → Option α} :
    ∀ {l : List α}, (∀ a ∈ l, f a = g a) → l.lookmap f = l.lookmap g
  | [], _ => rfl
  | a :: l, H => by
    obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
    rcases h : g a with - | b
    · simp [h, H₁.trans h, lookmap_congr H₂]
    · simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

Proof state:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H

Result:
case intro
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Proof state:
case intro.some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

Result:
no goals

Proof state:
case intro.none
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
h : g a = none
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
simp [h, H₁.trans h, lookmap_congr H₂]

Result:
no goals

Proof state:
case intro
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
rcases h : g a with - | b

Result:
case intro.none
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
h : g a = none
⊢ lookmap f (a :: l) = lookmap g (a :: l)

case intro.some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)