harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
  | ⟨k, e⟩ => by
    revert h
    rw [e]
    match k with
    | 0 => intro hn; simp at hn
    | pk+1 =>
      intro
      have := Nat.mul_le_mul_left m (succ_pos pk)
      rwa [Nat.mul_one] at this

Proof state:
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
⊢ m ≤ m * (pk + 1)

Tactic:
have := Nat.mul_le_mul_left m (succ_pos pk)

Result:
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
this : m * succ 0 ≤ m * pk.succ
⊢ m ≤ m * (pk + 1)

Proof state:
m n k pk : Nat
e : n = m * (pk + 1)
⊢ 0 < m * (pk + 1) → m ≤ m * (pk + 1)

Tactic:
intro

Result:
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
⊢ m ≤ m * (pk + 1)

Proof state:
m n k : Nat
e : n = m * 0
⊢ 0 < m * 0 → m ≤ m * 0

Tactic:
intro hn

Result:
m n k : Nat
e : n = m * 0
hn : 0 < m * 0
⊢ m ≤ m * 0

Proof state:
m n : Nat
h : 0 < n
k : Nat
e : n = m * k
⊢ m ≤ n

Tactic:
revert h

Result:
m n k : Nat
e : n = m * k
⊢ 0 < n → m ≤ n

Proof state:
m n k pk : Nat
e : n = m * (pk + 1)
h✝ : 0 < m * (pk + 1)
this : m * succ 0 ≤ m * pk.succ
⊢ m ≤ m * (pk + 1)

Tactic:
rwa [Nat.mul_one] at this

Result:
no goals

Proof state:
m n k : Nat
e : n = m * k
⊢ 0 < n → m ≤ n

Tactic:
rw [e]

Result:
m n k : Nat
e : n = m * k
⊢ 0 < m * k → m ≤ m * k

Proof state:
m n k : Nat
e : n = m * k
⊢ 0 < m * k → m ≤ m * k

Tactic:
match k with
| 0 => intro hn; simp at hn
| pk+1 =>
  intro
  have := Nat.mul_le_mul_left m (succ_pos pk)
  rwa [Nat.mul_one] at this

Result:
no goals

Proof state:
m n k : Nat
e : n = m * 0
hn : 0 < m * 0
⊢ m ≤ m * 0

Tactic:
simp at hn

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Basis.card_le_card_of_linearIndependent {ι : Type*} [Fintype ι] (b : Basis ι R M)
    {ι' : Type*} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) :
    Fintype.card ι' ≤ Fintype.card ι

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
ι' : Type u_2
inst✝ : Fintype ι'
v : ι' → M
hv : LinearIndependent R v
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ Fintype.card ι' ≤ Fintype.card ι

Tactic:
simpa [rank_eq_card_basis b, Cardinal.mk_fintype] using hv.cardinal_lift_le_rank

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
ι' : Type u_2
inst✝ : Fintype ι'
v : ι' → M
hv : LinearIndependent R v
⊢ Fintype.card ι' ≤ Fintype.card ι

Tactic:
letI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
ι' : Type u_2
inst✝ : Fintype ι'
v : ι' → M
hv : LinearIndependent R v
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ Fintype.card ι' ≤ Fintype.card ι
-- Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Proof state:
case inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommGroup (E i)
inst✝⁷ : (i : ι) → Module 𝕜 (E i)
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ ∃ a, (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap a = f

Tactic:
use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f

Result:
case h
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommGroup (E i)
inst✝⁷ : (i : ι) → Module 𝕜 (E i)
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap
      ((SeparationQuotient.outCLM 𝕜 F).compContinuousMultilinearMap f) =
    f
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive (attr := simp)]
lemma antilipschitzWith_inv_iff : AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

Tactic:
simp [AntilipschitzWith]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem Fin.snoc_eq_cons_rotate {α : Type*} (v : Fin n → α) (a : α) :
    @Fin.snoc _ (fun _ => α) v a = fun i => @Fin.cons _ (fun _ => α) a v (finRotate _ i)

Proof state:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
subst h''

Result:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a ⟨n, h⟩ = cons a v ((finRotate (n + 1)) ⟨n, h⟩)

Proof state:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i

Tactic:
exact (Nat.eq_of_le_of_lt_succ h' h).symm

Result:
no goals

Proof state:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']

Result:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ cast ⋯ (v (⟨i, h⟩.castLT h')) = cases a v ⟨i + 1, ⋯⟩

Proof state:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
have h'' : n = i := by
  simp only [not_lt] at h'
  exact (Nat.eq_of_le_of_lt_succ h' h).symm

Result:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Proof state:
case h.mk
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
by_cases h' : i < n

Result:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Proof state:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i

Tactic:
simp only [not_lt] at h'

Result:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i

Proof state:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ cast ⋯ (v (⟨i, h⟩.castLT h')) = cases a v ⟨i + 1, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i => cons a v ((finRotate (n + 1)) i)

Tactic:
ext ⟨i, h⟩

Result:
case h.mk
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Proof state:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ cast ⋯ a = cases a v ⟨0, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a ⟨n, h⟩ = cons a v ((finRotate (n + 1)) ⟨n, h⟩)

Tactic:
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]

Result:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ cast ⋯ a = cases a v ⟨0, ⋯⟩
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_div_of_neg_of_lt (hc : c < 0) (h : b < a) : a / c < b / c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
h : b < a
⊢ a / c < b / c

Tactic:
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
h : b < a
⊢ a * (1 / c) < b * (1 / c)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
h : b < a
⊢ a * (1 / c) < b * (1 / c)

Tactic:
exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)

Result:
no goals
-- Mathlib/Control/Basic.lean
theorem guard_false {h : Decidable False} : @guard F _ False h = failure

Proof state:
F : Type → Type v
inst✝ : Alternative F
h : Decidable False
⊢ guard False = failure

Tactic:
simp [guard, if_neg not_false]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_inter (l l' : List α) : (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∩ l').toFinset ↔ a✝ ∈ l.toFinset ∩ l'.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∩ l').toFinset ↔ a✝ ∈ l.toFinset ∩ l'.toFinset
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} :
    c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h : c.fst < w.length, c.snd < w[c.fst]

Proof state:
w : List ℕ
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ (h : c.1 < w.length), c.2 < w[c.1]

Tactic:
induction w generalizing c <;> rw [YoungDiagram.cellsOfRowLens]

Result:
case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]

Proof state:
case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

Tactic:
simp [YoungDiagram.cellsOfRowLens]

Result:
no goals

Proof state:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]

Tactic:
rcases c with ⟨⟨_, _⟩, _⟩ <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_prime {p : ℕ} (hp : Nat.Prime p) : p.primeFactorsList = [p]

Proof state:
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : p.minFac = p
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Tactic:
simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Tactic:
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2

Result:
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : p.minFac = p
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Proof state:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.primeFactorsList = [p]

Tactic:
rw [this, primeFactorsList]

Result:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]

Proof state:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]

Tactic:
simp only [Eq.symm this]

Result:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Proof state:
p : ℕ
hp : Prime p
⊢ p.primeFactorsList = [p]

Tactic:
have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl

Result:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.primeFactorsList = [p]
-- Mathlib/Analysis/Seminorm.lean
theorem sSup_empty : sSup (∅ : Set (Seminorm 𝕜 E)) = ⊥

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ (sSup ∅) x✝ = ⊥ x✝

Tactic:
rw [Seminorm.sSup_apply bddAbove_empty, Real.iSup_of_isEmpty]

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ 0 = ⊥ x✝

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ 0 = ⊥ x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ sSup ∅ = ⊥

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ (sSup ∅) x✝ = ⊥ x✝
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem integerSetToAssociates_surjective :
    Function.Surjective (integerSetToAssociates K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective (integerSetToAssociates K)

Tactic:
rintro ⟨x⟩

Result:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x

Proof state:
case mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x

Tactic:
refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
  Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩

Result:
case mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩ * ↑(unitsNonZeroDivisorsEquiv.symm u⁻¹) = x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ (mixedEmbedding K) ↑↑x ≠ 0

Tactic:
exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ u, u • (mixedEmbedding K) ↑↑x ∈ integerSet K

Tactic:
refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ (mixedEmbedding K) ↑↑x ≠ 0

Proof state:
case mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩ * ↑(unitsNonZeroDivisorsEquiv.symm u⁻¹) = x

Tactic:
simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
  Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
  unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
  Units.mul_inv_cancel_right]

Result:
no goals

Proof state:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x

Tactic:
obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by
  refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
  exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Result:
case mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ ∃ a, integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰)) x
-- Mathlib/Data/Matrix/Mul.lean
theorem zero_mulVec [Fintype n] (v : n → α) : (0 : Matrix m n α) *ᵥ v = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
⊢ 0 *ᵥ v = 0

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝

Tactic:
simp [mulVec]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem forall_forall_merge' (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) (z : β) :
    (∀ j i : ℕ, (c₀ i) (c₁ j) ≤ z) ↔ ∀ i : ℕ, (c₀ i) (c₁ i) ≤ z

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

Tactic:
rw [forall_swap, forall_forall_merge]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_two : fastGrowing 2 = fun n => (2 ^ n) * n

Proof state:
case h
i a b : ℕ
⊢ (fun n => 2 * n)^[a] b = 2 ^ a * b

Tactic:
induction a <;>
simp [*, Function.iterate_succ, pow_succ, mul_assoc, -Function.iterate_succ]

Result:
no goals

Proof state:
⊢ (fun i => (fastGrowing 1)^[i] i) = fun n => 2 ^ n * n

Tactic:
funext i

Result:
case h
i : ℕ
⊢ (fastGrowing 1)^[i] i = 2 ^ i * i

Proof state:
case h
i : ℕ
⊢ (fun n => 2 * n)^[i] i = 2 ^ i * i

Tactic:
suffices ∀ a b, (fun n : ℕ => 2 * n)^[a] b = (2 ^ a) * b from this _ _

Result:
case h
i : ℕ
⊢ ∀ (a b : ℕ), (fun n => 2 * n)^[a] b = 2 ^ a * b

Proof state:
case h
i : ℕ
⊢ ∀ (a b : ℕ), (fun n => 2 * n)^[a] b = 2 ^ a * b

Tactic:
intro a b

Result:
case h
i a b : ℕ
⊢ (fun n => 2 * n)^[a] b = 2 ^ a * b

Proof state:
⊢ fastGrowing 2 = fun n => 2 ^ n * n

Tactic:
rw [@fastGrowing_succ 2 1 rfl]

Result:
⊢ (fun i => (fastGrowing 1)^[i] i) = fun n => 2 ^ n * n

Proof state:
case h
i : ℕ
⊢ (fastGrowing 1)^[i] i = 2 ^ i * i

Tactic:
rw [fastGrowing_one]

Result:
case h
i : ℕ
⊢ (fun n => 2 * n)^[i] i = 2 ^ i * i
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoc_comm (a b : α) : Ι a b = Ι b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ι a b = Ι b a

Tactic:
simp only [uIoc, min_comm a b, max_comm a b]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_lt_sub_one_of_pos (hx1 : 0 < x) (hx2 : x ≠ 1) : log x < x - 1

Proof state:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x ≠ 0

Tactic:
rwa [← log_one, log_injOn_pos.ne_iff hx1]

Result:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0

Proof state:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0

Tactic:
exact mem_Ioi.mpr zero_lt_one

Result:
no goals

Proof state:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1

Tactic:
have h : log x ≠ 0 := by
  rwa [← log_one, log_injOn_pos.ne_iff hx1]
  exact mem_Ioi.mpr zero_lt_one

Result:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1

Proof state:
x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
h : log x ≠ 0
⊢ log x < x - 1

Tactic:
linarith [add_one_lt_exp h, exp_log hx1]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem linear_proj_add_linearProjOfIsCompl_eq_self (hpq : IsCompl p q) (x : E) :
    (p.linearProjOfIsCompl q hpq x + q.linearProjOfIsCompl p hpq.symm x : E) = x

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ ↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) +
      ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq).symm) x) =
    x

Tactic:
exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ ↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) +
      ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(q.prodEquivOfIsCompl p ⋯).symm) x) =
    x

Tactic:
rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ ↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) +
      ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq).symm) x) =
    x

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ ↑((p.linearProjOfIsCompl q hpq) x) + ↑((q.linearProjOfIsCompl p ⋯) x) = x

Tactic:
dsimp only [linearProjOfIsCompl]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ ↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) +
      ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(q.prodEquivOfIsCompl p ⋯).symm) x) =
    x
-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma sum_Ico_le_integral_of_le
    (hab : a ≤ b) (h : ∀ i ∈ Ico a b, ∀ x ∈ Ico (i : ℝ) (i + 1 : ℕ), f i ≤ g x)
    (hg : IntegrableOn g (Set.Ico a b)) :
    ∑ i ∈ Finset.Ico a b, f i ≤ ∫ x in a..b, g x

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
calc
∑ i ∈ Finset.Ico a b, f i
_ = ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), f i) := by simp
_ ≤ ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), g x) := by
  apply Finset.sum_le_sum (fun i hi ↦ ?_)
  apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
  exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
_ = ∫ x in a..b, g x := by
  rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
  intro i hi
  exact A _ (by simpa using hi)

Result:
no goals

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ Ico ↑i ↑(i + 1) ⊆ Ico ↑a ↑b

Tactic:
rintro x ⟨hx, h'x⟩

Result:
case intro
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
x : ℝ
hx : ↑i ≤ x
h'x : x < ↑(i + 1)
⊢ x ∈ Ico ↑a ↑b
-- Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
@[simp, reassoc]
lemma induced_isoShiftZero_hom_app_obj (X : C) :
    letI := (induced e M F' e')
    (F.isoShiftZero M).hom.app (L.obj X) =
      (e' 0).hom.app X ≫ (isoShiftZero G M).hom.app X ≫ e.inv.app X

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_7, u_1} C
inst✝⁸ : Category.{u_6, u_2} D
inst✝⁷ : Category.{u_5, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
X : C
⊢ (F.isoShiftZero M).hom.app (L.obj X) = (e' 0).hom.app X ≫ (G.isoShiftZero M).hom.app X ≫ e.inv.app X

Tactic:
apply induced.isoZero_hom_app_obj

Result:
no goals