harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem le_inf {a b c : CauSeq α abs} (hb : a ≤ b) (hc : a ≤ c) : a ≤ b ⊓ c

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c

Tactic:
exact Setoid.symm (CauSeq.inf_eq_left hc)

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a ≤ b ⊓ c

Tactic:
exact Or.inl (CauSeq.lt_inf hb hc)

Result:
no goals

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c

Tactic:
refine le_of_eq_of_le hc (Or.inr ?_)

Result:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c

Tactic:
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le

Result:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c

Tactic:
exact Setoid.symm (CauSeq.inf_eq_right hb)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c

Tactic:
replace hc := le_of_eq_of_le (Setoid.symm hb) hc

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c

Tactic:
refine le_of_eq_of_le hb (Or.inr ?_)

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≤ b
hc : a ≤ c
⊢ a ≤ b ⊓ c

Tactic:
obtain hb | hb := hb

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c

Tactic:
obtain hc | hc := hc

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a ≤ b ⊓ c

case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :
    ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

Proof state:
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

Tactic:
rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_boole_mul [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
    𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i

Proof state:
case ha
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ ↑(Fintype.card ι) ≠ 0

Tactic:
simp [Fintype.card_ne_zero]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ 𝔼 j : ι, (if i = j then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]

Result:
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ (↑(Fintype.card ι))⁻¹ • (↑(Fintype.card ι) * f i) = f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ (↑(Fintype.card ι))⁻¹ • (↑(Fintype.card ι) * f i) = f i

Tactic:
rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]

Result:
case ha
ι : Type u_1
M : Type u_3
inst✝⁴ : Semifield M
inst✝³ : CharZero M
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → M
i : ι
⊢ ↑(Fintype.card ι) ≠ 0
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem dvdNotUnit_of_dvdNotUnit_associated [CommMonoidWithZero M] [Nontrivial M] {p q r : M}
    (h : DvdNotUnit p q) (h' : Associated q r) : DvdNotUnit p r

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨u, rfl⟩ := Associated.symm h'

Result:
case intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h : DvdNotUnit p (r * ↑u)
h' : r * ↑u ~ᵤ r
⊢ DvdNotUnit p r

Proof state:
case intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h : DvdNotUnit p (r * ↑u)
h' : r * ↑u ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨hp, x, hx⟩ := h

Result:
case intro.intro.intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ DvdNotUnit p r

Proof state:
case intro.intro.intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ r = p * (x * ↑u⁻¹)

Tactic:
rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]

Result:
no goals

Proof state:
case intro.intro.intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ DvdNotUnit p r

Tactic:
refine ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩

Result:
case intro.intro.intro
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : Nontrivial M
p r : M
u : Mˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ r = p * (x * ↑u⁻¹)
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
    (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}

Proof state:
case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ f ∉ σ.cycleFactorsFinset

Tactic:
exact fun H =>
not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : ¬f x = x
⊢ (τ * f⁻¹) x = x

Tactic:
rw [mul_apply]

Result:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : ¬f x = x
⊢ τ (f⁻¹ x) = x

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    σ.IsCycle → fun {g} =>
      ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}

Tactic:
intro σ hσ f hf

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : σ.IsCycle
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_X_pow {n : ℕ} : (X ^ n).eval₂ f x = x ^ n

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (X ^ n) = x ^ n

Tactic:
rw [X_pow_eq_monomial]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ((monomial n) 1) = x ^ n

Proof state:
case h.e'_3
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ x ^ n = f 1 * x ^ n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ((monomial n) 1) = x ^ n

Tactic:
convert eval₂_monomial f x (n := n) (r := 1)

Result:
case h.e'_3
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ x ^ n = f 1 * x ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Basic.lean
theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
  ⟨fun h => by cases h; assumption, Lex.inl⟩

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
a₁ a₂ : α✝
h : Lex r s (inl a₁) (inl a₂)
⊢ r a₁ a₂

Tactic:
cases h

Result:
case inl
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
a₁ a₂ : α✝
h✝ : r a₁ a₂
⊢ r a₁ a₂

Proof state:
case inl
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
a₁ a₂ : α✝
h✝ : r a₁ a₂
⊢ r a₁ a₂

Tactic:
assumption

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma partSize_eq_one_of_range_emb_eq_singleton
    (c : OrderedFinpartition n) {i : Fin c.length} {j : Fin n}
    (hc : range (c.emb i) = {j}) :
    c.partSize i = 1

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
this : Fintype.card ↑(range (c.emb i)) = Fintype.card (Fin (c.partSize i))
⊢ c.partSize i = 1

Tactic:
simpa [hc] using this.symm

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
⊢ c.partSize i = 1

Tactic:
have : Fintype.card (range (c.emb i)) = Fintype.card (Fin (c.partSize i)) :=
  card_range_of_injective (c.emb_strictMono i).injective

Result:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
this : Fintype.card ↑(range (c.emb i)) = Fintype.card (Fin (c.partSize i))
⊢ c.partSize i = 1
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_map (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) (z : R[X]) :
    h.aequiv h' (h.map z) = h'.map z

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.aequiv h') (h.map z) = h'.map z

Tactic:
rw [aequiv, AlgEquiv.coe_mk, Equiv.coe_fn_mk, liftHom_map, aeval_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem measurableSet_cut (r : α → β → Prop) (f : α →ₛ β) (h : ∀ b, MeasurableSet { a | r a b }) :
    MeasurableSet { a | r a (f a) }

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
this : r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i
⊢ a ∈ {a | r a (f a)} ↔ a ∈ ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet {a | r a (f a)}

Tactic:
rw [this]

Result:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet (⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b})

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i

Tactic:
exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ a ∈ {a | r a (f a)} ↔ a ∈ ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet (⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b})

Tactic:
exact
  MeasurableSet.biUnion f.finite_range.countable fun b _ =>
    MeasurableSet.inter (h b) (f.measurableSet_fiber _)

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ a ∈ {a | r a (f a)} ↔ a ∈ ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ MeasurableSet {a | r a (f a)}

Tactic:
have : { a | r a (f a) } = ⋃ b ∈ range f, { a | r a b } ∩ f ⁻¹' {b} := by
  ext a
  suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
  exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet {a | r a (f a)}
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_natDegree_le (f : R[X]) : f.reverse.natDegree ≤ f.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0

Tactic:
rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
  coeff_eq_zero_of_natDegree_lt hn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0

Tactic:
intro n hn

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : ↑f.natDegree < ↑n
⊢ f.reverse.coeff n = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natDegree ≤ f.natDegree

Tactic:
rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : ↑f.natDegree < ↑n
⊢ f.reverse.coeff n = 0

Tactic:
rw [Nat.cast_lt] at hn

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0
-- Mathlib/Algebra/Group/Pi/Lemmas.lean
theorem uncurry_mulSingle_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
    (a : α) (b : β a) (x : γ a b) :
    Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle (Sigma.mk a b) x

Proof state:
α : Type u_3
β : α → Type u_4
γ : (a : α) → β a → Type u_5
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
⊢ uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x

Tactic:
rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]

Result:
no goals
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem closure_residualEq {s : Set α} (hs : IsLocallyClosed s) : closure s =ᵇ s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ closure s =ᶠ[residual α] s

Tactic:
rw [Filter.eventuallyEq_set]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ ∀ᵇ (x : α), x ∈ closure s ↔ x ∈ s

Proof state:
case h
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure s ↔ x ∈ s

Tactic:
nth_rewrite 2 [← closure_inter_coborder (s := s)]

Result:
case h
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure s ↔ x ∈ closure s ∩ coborder s

Proof state:
case h
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure s ↔ x ∈ closure s ∩ coborder s

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ ∀ᵇ (x : α), x ∈ closure s ↔ x ∈ s

Tactic:
filter_upwards [coborder_mem_residual hs] with x hx

Result:
case h
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure s ↔ x ∈ s
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma symm {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : LeftFractionRel z₁ z₂) :
    LeftFractionRel z₂ z₁

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₂ z₁

Tactic:
exact ⟨Z, t₂, t₁, hst.symm, hft.symm, by simpa only [← hst] using ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ W (z₂.s ≫ t₂)

Tactic:
simpa only [← hst] using ht

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ LeftFractionRel z₂ z₁

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₂ z₁
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.ne_zero_or_ne_zero [Nontrivial R] (h : IsCoprime x y) : x ≠ 0 ∨ y ≠ 0

Proof state:
case a
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Result:
no goals

Proof state:
case a
R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0

Tactic:
rintro rfl rfl

Result:
case a
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False

Proof state:
R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
apply not_or_of_imp

Result:
case a
R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated map_smul_of_iInf_genEigenspace_ne_bot (since := "2024-10-23")]
lemma map_smul_of_iInf_iSup_genEigenspace_ne_bot [NoZeroSMulDivisors R M]
    {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
    (μ : L → R) (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥)
    (t : R) (x : L) :
    μ (t • x) = t • μ x

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
t : R
x : L
h_ne : ⨅ x, (f x).maxGenEigenspace (μ x) ≠ ⊥
⊢ μ (t • x) = t • μ x

Tactic:
apply map_smul_of_iInf_genEigenspace_ne_bot f μ ⊤ h_ne t x

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) ↑k ≠ ⊥
t : R
x : L
⊢ μ (t • x) = t • μ x

Tactic:
simp_rw [iSup_genEigenspace_eq] at h_ne

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
t : R
x : L
h_ne : ⨅ x, (f x).maxGenEigenspace (μ x) ≠ ⊥
⊢ μ (t • x) = t • μ x
-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem exists_mem_finsetApprox (a : S) {b} (hb : b ≠ (0 : R)) :
    ∃ q : S,
      ∃ r ∈ finsetApprox bS adm, abv (Algebra.norm R (r • a - b • q)) <
      abv (Algebra.norm R (algebraMap R S b))

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
hμ : μ = distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
have hjk' : ∀ i, (abv (rs k i - rs j i) : ℝ) < abv b • ε := by simpa only [r_eq] using hjk

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
hμ : μ = distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))