harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma le_truncatedSup : a ≤ truncatedSup s a

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
⊢ a ≤ if h : a ∈ lowerClosure ↑s then (filter (fun b => a ≤ b) s).sup' ⋯ id else ⊤

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
h : a ∈ lowerClosure ↑s
⊢ a ≤ (filter (fun b => a ≤ b) s).sup' ⋯ id

case neg
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
h : a ∉ lowerClosure ↑s
⊢ a ≤ ⊤

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
⊢ a ≤ s.truncatedSup a

Tactic:
rw [truncatedSup]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
⊢ a ≤ if h : a ∈ lowerClosure ↑s then (filter (fun b => a ≤ b) s).sup' ⋯ id else ⊤

Proof state:
case neg
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
h : a ∉ lowerClosure ↑s
⊢ a ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
h : a ∈ lowerClosure ↑s
⊢ a ≤ (filter (fun b => a ≤ b) s).sup' ⋯ id

Tactic:
obtain ⟨ℬ, hb, h⟩ := h

Result:
case pos.intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
ℬ : α
hb : ℬ ∈ ↑s
h : a ≤ ℬ
⊢ a ≤ (filter (fun b => a ≤ b) s).sup' ⋯ id

Proof state:
case pos.intro.intro
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
ℬ : α
hb : ℬ ∈ ↑s
h : a ≤ ℬ
⊢ a ≤ (filter (fun b => a ≤ b) s).sup' ⋯ id

Tactic:
exact h.trans <| le_sup' id <| mem_filter.2 ⟨hb, h⟩

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma binomial_sum_eq (h : n < m) :
    ∑ i ∈ range (n + 1), (n.choose i * (m - n) / ((m - i) * m.choose i) : ℚ) = 1

Proof state:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose (i + 1)))⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]

Result:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
-- Mathlib/SetTheory/Lists.lean
theorem subset_nil {l : Lists' α true} : l ⊆ Lists'.nil → l = Lists'.nil

Proof state:
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil

Tactic:
rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ nil → ofList l.toList = nil

Tactic:
induction toList l <;> intro h

Result:
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil

case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil

Proof state:
α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil

Tactic:
rw [← of_toList l]

Result:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ nil → ofList l.toList = nil
-- Mathlib/Data/List/Dedup.lean
theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f)
    (xs : List α) :
    (xs.map f).dedup = xs.dedup.map f

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∉ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_not_mem h, dedup_cons_of_not_mem <| (mem_map_of_injective hf).not.mpr h, ih,
  map_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (map f (x :: xs)).dedup = map f (x :: xs).dedup

Tactic:
rw [map_cons]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem f h), ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
by_cases h : x ∈ xs

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∉ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Proof state:
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
⊢ (map f []).dedup = map f [].dedup

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem lex_def {r : α → α → Prop} {s : β → β → Prop} {p q : α × β} :
    Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
  ⟨fun h => by cases h <;> simp [*], fun h =>
    match p, q, h with
    | _, _, Or.inl h => Lex.left _ _ h
    | (_, _), (_, _), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
p q : α × β
h : Prod.Lex r s p q
⊢ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd

Tactic:
cases h <;> simp [*]

Result:
no goals

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
fst✝ : α
snd✝¹ snd✝ : β
h : s { fst := fst✝, snd := snd✝¹ }.snd { fst := { fst := fst✝, snd := snd✝¹ }.fst, snd := snd✝ }.snd
⊢ Prod.Lex r s { fst := fst✝, snd := snd✝¹ } { fst := { fst := fst✝, snd := snd✝¹ }.fst, snd := snd✝ }

Tactic:
exact Lex.right _ h

Result:
no goals

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
e : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h : s { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ Prod.Lex r s { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ }

Tactic:
subst e

Result:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
fst✝ : α
snd✝¹ snd✝ : β
h : s { fst := fst✝, snd := snd✝¹ }.snd { fst := { fst := fst✝, snd := snd✝¹ }.fst, snd := snd✝ }.snd
⊢ Prod.Lex r s { fst := fst✝, snd := snd✝¹ } { fst := { fst := fst✝, snd := snd✝¹ }.fst, snd := snd✝ }
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_ae_eq_condExpL1CLM (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) :
    μ[f|m] =ᵐ[μ] condExpL1CLM E hm μ (hf.toL1 f)

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
x : α
⊢ ↑↑(condExpL1 hm μ f) x = ↑↑((condExpL1CLM E hm μ) (Integrable.toL1 f hf)) x

Tactic:
rw [condExpL1_eq hf]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ μ[f|m] =ᶠ[ae μ] ↑↑((condExpL1CLM E hm μ) (Integrable.toL1 f hf))

Tactic:
refine (condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)

Result:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
x : α
⊢ ↑↑(condExpL1 hm μ f) x = ↑↑((condExpL1CLM E hm μ) (Integrable.toL1 f hf)) x
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.commute_iff' {g c : Perm α} (hc : c.IsCycle) :
    Commute g c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ g x ∈ c.support,
        subtypePerm g hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Proof state:
case h.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ ↑((c.subtypePerm ⋯ ^ i) ⟨x, hx⟩) = g x

Tactic:
rw [subtypePerm_apply_zpow_of_mem]

Result:
case h.H.mk.a
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ (c ^ i) x = g x

Proof state:
case mpr.intro.intro.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ (g * c) x = (c * g) x

Tactic:
simp only [coe_mul, Function.comp_apply]

Result:
case mpr.intro.intro.H
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
i : ℤ
hi : (fun x => c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ g (c x) = c (g x)

Proof state:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i) a = g a

Tactic:
exact hi

Result:
no goals

Proof state:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)

Tactic:
simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]

Result:
case h.H.mk.a.intro
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ c.support ↔ g x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_size {a : Array α} : a[a.size]? = none

Proof state:
α : Type u_1
a : Array α
⊢ a[a.size]? = none

Tactic:
simp only [getElem?_def, Nat.lt_irrefl, dite_false]

Result:
no goals
-- Mathlib/NumberTheory/SiegelsLemma.lean
theorem exists_ne_zero_int_vec_norm_le
    (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) : ∃ t : β → ℤ, t ≠ 0 ∧
    A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * max 1 ‖A‖) ^ ((m : ℝ) / (n - m))

Proof state:
case intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ (fun x => ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊) i ≤
    ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i

Tactic:
simp only [le_add_iff_nonneg_right]

Result:
case intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ 0 ≤ y i

Proof state:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ 0 ≤ x i

Tactic:
exact hxT.1 i

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ B' i ≤ x i + ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
norm_cast

Result:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ (fun x => ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊) i ≤
    x i + ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ ‖x - y‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Tactic:
have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ ‖x - y‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
-- Mathlib/Algebra/Group/Submonoid/Finsupp.lean
theorem mem_closure_range_iff :
    x ∈ closure (Set.range f) ↔ ∃ a : ι →₀ ℕ, x = a.prod (f · ^ ·)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) → x ∈ closure (Set.range f)

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Result:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) → x ∈ closure (Set.range f)

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)

Tactic:
exact prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem left_cancel (x : R) {y y' : R} : x ◃ y = x ◃ y' ↔ y = y'

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃ y = x ◃ y'

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ y = x ◃ y

Proof state:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' → y = y'

Tactic:
apply (act' x).injective

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ y = x ◃ y

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' ↔ y = y'

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' → y = y'

case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃ y = x ◃ y'
-- Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean
lemma finite_real_spectrum : (spectrum ℝ A).Finite

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
⊢ (⇑(algebraMap ℝ 𝕜) ⁻¹' spectrum 𝕜 A).Finite

Tactic:
exact A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
⊢ (spectrum ℝ A).Finite

Tactic:
rw [← spectrum.preimage_algebraMap 𝕜]

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
⊢ (⇑(algebraMap ℝ 𝕜) ⁻¹' spectrum 𝕜 A).Finite
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_insert_left [DecidableEq α] :
    image₂ f (insert a s) t = (t.image fun b => f a b) ∪ image₂ f s t :=
  coe_injective <| by
    push_cast
    exact image2_insert_left

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image2 f (insert a ↑s) ↑t = (fun b => f a b) '' ↑t ∪ image2 f ↑s ↑t

Tactic:
exact image2_insert_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ ↑(image₂ f (insert a s) t) = ↑(image (fun b => f a b) t ∪ image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image2 f (insert a ↑s) ↑t = (fun b => f a b) '' ↑t ∪ image2 f ↑s ↑t
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem rpow_logb_of_neg (hx : x < 0) : b ^ logb b x = -x

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ b ^ logb b x = -x

Tactic:
rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]

Result:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x

Tactic:
exact abs_of_neg hx

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : (𝓝[s \ {x}] x).NeBot) :
    0 ∈ tangentConeAt 𝕜 s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
⊢ Tendsto (fun n => ‖c n‖⁻¹) atTop (𝓝[>] 0)

Tactic:
simp only [nhdsWithin, tendsto_inf, tendsto_principal, mem_Ioi, norm_pos_iff, ne_eq,
  eventually_atTop, ge_iff_le]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n * u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < u n
le_c : ∀ (n : ℕ), u n / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ (u n)⁻¹ * ‖r‖ * ‖d n‖
⊢ Tendsto (fun n => ‖c n‖⁻¹) atTop (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → 0 < ‖c b‖⁻¹
-- Mathlib/Computability/ContextFreeGrammar.lean
/-- Add extra prefix to context-free rewriting. -/
lemma Rewrites.append_left (hvw : r.Rewrites u v) (p : List (Symbol T N)) :
    r.Rewrites (p ++ u) (p ++ v)

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Tactic:
rcases hvw with ⟨x, y, hxy⟩

Result:
case intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Proof state:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y

Tactic:
simp_all

Result:
no goals

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (p ++ u) (p ++ v)

Tactic:
rw [rewrites_iff] at *

Result:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Proof state:
case intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Tactic:
use p ++ x, y

Result:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem top_orthogonal_eq_bot : (⊤ : Submodule 𝕜 E)ᗮ = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊤ᗮ = ⊥

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ ⊤ᗮ ↔ x ∈ ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x = 0 → ∀ u ∈ ⊤, inner u x = 0

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ∀ u ∈ ⊤, inner u 0 = 0

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ (∀ u ∈ ⊤, inner u x = 0) ↔ x = 0

Tactic:
exact
  ⟨fun h => inner_self_eq_zero.mp (h x mem_top), by
    rintro rfl
    simp⟩

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ ⊤ᗮ ↔ x ∈ ⊥

Tactic:
rw [mem_bot, mem_orthogonal]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ (∀ u ∈ ⊤, inner u x = 0) ↔ x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ∀ u ∈ ⊤, inner u 0 = 0

Tactic:
simp

Result:
no goals