harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_replicate_self : (replicate n a).set i a = replicate n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ (replicate n a).set i a = replicate n a

Tactic:
apply ext_getElem

Result:
case hl
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((replicate n a).set i a).length = (replicate n a).length

case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((replicate n a).set i a).length) (h₂ : i_1 < (replicate n a).length),
    ((replicate n a).set i a)[i_1] = (replicate n a)[i_1]

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
i✝ i : Nat
h₁ : i < ((replicate n a).set i✝ a).length
h₂ : i < (replicate n a).length
⊢ ((replicate n a).set i✝ a)[i] = (replicate n a)[i]

Tactic:
simp [getElem_set]

Result:
no goals

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((replicate n a).set i a).length) (h₂ : i_1 < (replicate n a).length),
    ((replicate n a).set i a)[i_1] = (replicate n a)[i_1]

Tactic:
intro i h₁ h₂

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
i✝ i : Nat
h₁ : i < ((replicate n a).set i✝ a).length
h₂ : i < (replicate n a).length
⊢ ((replicate n a).set i✝ a)[i] = (replicate n a)[i]

Proof state:
case hl
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((replicate n a).set i a).length = (replicate n a).length

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_last_apply (i : Fin n) : succAbove (last n) i = castSucc i

Proof state:
n : ℕ
i : Fin n
⊢ (last n).succAbove i = i.castSucc

Tactic:
rw [succAbove_last]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_sum_nat_add (f : ℕ → ℝ≥0∞) (hf : ∑' i, f i ≠ ∞) :
    Tendsto (fun i => ∑' k, f (k + i)) atTop (𝓝 0)

Proof state:
case intro
f : ℕ → ℝ≥0
hf : ∑' (i : ℕ), (fun i => ↑(f i)) i ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)

Tactic:
replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf

Result:
case intro
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)

Proof state:
f : ℕ → ℝ≥0∞
hf : ∑' (i : ℕ), f i ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf

Result:
case intro
f : ℕ → ℝ≥0
hf : ∑' (i : ℕ), (fun i => ↑(f i)) i ≠ ⊤
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)

Proof state:
case intro
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)

Tactic:
simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]

Result:
case intro
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)

Proof state:
case intro
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i => ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)

Tactic:
exact mod_cast NNReal.tendsto_sum_nat_add f

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_prod_le (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
    range (prod f g) ≤ (range f).prod (range g)

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
x : M
⊢ (∃ y, f y = (Pi.prod (⇑f) (⇑g) x).1) ∧ ∃ y, g y = (Pi.prod (⇑f) (⇑g) x).2

Tactic:
exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ range (f.prod g) ≤ (range f).prod (range g)

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, SetLike.mem_coe, mem_prod, exists_imp]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ ∀ ⦃x : M₂ × M₃⦄ (x_1 : M), Pi.prod (⇑f) (⇑g) x_1 = x → (∃ y, f y = x.1) ∧ ∃ y, g y = x.2

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ ∀ ⦃x : M₂ × M₃⦄ (x_1 : M), Pi.prod (⇑f) (⇑g) x_1 = x → (∃ y, f y = x.1) ∧ ∃ y, g y = x.2

Tactic:
rintro _ x rfl

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
x : M
⊢ (∃ y, f y = (Pi.prod (⇑f) (⇑g) x).1) ∧ ∃ y, g y = (Pi.prod (⇑f) (⇑g) x).2
-- Mathlib/Algebra/Group/End.lean
@[simp] lemma pow_addRight (n : ℕ) : Equiv.addRight a ^ n = Equiv.addRight (n • a)

Proof state:
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
⊢ Equiv.addRight a ^ n = Equiv.addRight (n • a)

Tactic:
ext

Result:
case H
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.addRight a ^ n) x✝ = (Equiv.addRight (n • a)) x✝

Proof state:
case H
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.addRight a ^ n) x✝ = (Equiv.addRight (n • a)) x✝

Tactic:
simp [Perm.coe_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem self_eq_add_right {x y : BitVec w} : x = x + y ↔ y = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x + y = x ↔ y = 0#w

Tactic:
exact BitVec.add_right_eq_self

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x = x + y ↔ y = 0#w

Tactic:
rw [Eq.comm]

Result:
w : Nat
x y : BitVec w
⊢ x + y = x ↔ y = 0#w
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem isClosed_setOf_lipschitzOnWith {α β} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0)
    (s : Set α) : IsClosed { f : α → β | LipschitzOnWith K f s }

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed {f | LipschitzOnWith K f s}

Tactic:
simp only [LipschitzOnWith, setOf_forall]

Result:
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed (⋂ i ∈ s, ⋂ i_1 ∈ s, {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed (⋂ i ∈ s, ⋂ i_1 ∈ s, {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})

Tactic:
refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_

Result:
case refine_1
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => edist (x_1 x) (x_1 y)

case refine_2
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => ↑K * edist x y

Proof state:
case refine_1
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => edist (x_1 x) (x_1 y)

case refine_2
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => ↑K * edist x y

Tactic:
exacts [.edist (continuous_apply x) (continuous_apply y), continuous_const]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem vanishingIdeal_closure (t : Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal (closure t) = vanishingIdeal t

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
exact this

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
ext1

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem orderIsoRpow_symm_apply (y : ℝ) (hy : 0 < y) :
    (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) (one_div_pos.2 hy)

Proof state:
y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]

Result:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯

Proof state:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) :
    ∃ maxLit, c.maxLiteral = some maxLit

Proof state:
l : Nat
c : Clause Nat
h : (l, false) ∈ c ∨ (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Tactic:
cases h <;> rename_i h

Result:
case inl
l : Nat
c : Clause Nat
h : (l, false) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Proof state:
l : Nat
c : Clause Nat
h : Mem l c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Tactic:
dsimp [Mem] at h

Result:
l : Nat
c : Clause Nat
h : (l, false) ∈ c ∨ (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Proof state:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
h2 : ¬(List.map (fun x => x.fst) c).max? = none ↔ ¬List.map (fun x => x.fst) c = []
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Tactic:
simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral]

Result:
no goals

Proof state:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit

Tactic:
have h1 := List.ne_nil_of_mem h

Result:
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
⊢ ∃ maxLit, c.maxLiteral = some maxLit
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma IsLocalizedModule.of_restrictScalars (S : Submonoid R)
    {N : Type*} [AddCommGroup N] [Module R N] [Module A M] [Module A N]
    [IsScalarTower R A M] [IsScalarTower R A N]
    (f : M →ₗ[A] N) [IsLocalizedModule S (f.restrictScalars R)] :
    IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f where
  map_units x

Proof state:
case mk.intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : R
hx : x ∈ ↑S
⊢ IsUnit ((algebraMap A (Module.End A N)) ↑⟨(algebraMap R A) x, ⋯⟩)

Tactic:
have := IsLocalizedModule.map_units (f.restrictScalars R) ⟨x, hx⟩

Result:
case mk.intro.intro
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : R
hx : x ∈ ↑S
this : IsUnit ((algebraMap R (Module.End R N)) ↑⟨x, hx⟩)
⊢ IsUnit ((algebraMap A (Module.End A N)) ↑⟨(algebraMap R A) x, ⋯⟩)
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_fract (s : Set α) :
    fract ⁻¹' s = ⋃ m : ℤ, (fun x => x - (m : α)) ⁻¹' (s ∩ Ico (0 : α) 1)

Proof state:
case h.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
m : ℤ
hms : x - ↑m ∈ s
hm0 : 0 ≤ x - ↑m
hm1 : x - ↑m < 1
⊢ fract x ∈ s

Tactic:
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Result:
case h.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s

Tactic:
rintro ⟨m, hms, hm0, hm1⟩

Result:
case h.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
m : ℤ
hms : x - ↑m ∈ s
hm0 : 0 ≤ x - ↑m
hm1 : x - ↑m < 1
⊢ fract x ∈ s

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1

Tactic:
refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
⊢ fract ⁻¹' s = ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
ext x

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
simp only [mem_preimage, mem_iUnion, mem_inter_iff]

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1

Proof state:
case h.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s

Tactic:
exact hms

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem add_den_dvd (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den * q₂.den

Proof state:
case h
q₁ q₂ : ℚ
⊢ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den

Tactic:
apply Nat.gcd_dvd_right

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ {
        num :=
          (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) / ↑((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯,
        reduced := ⋯ }.den ∣
    q₁.den * q₂.den

Tactic:
apply Nat.div_dvd_of_dvd

Result:
case h
q₁ q₂ : ℚ
⊢ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den

Proof state:
q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den * q₂.den

Tactic:
rw [add_def, normalize_eq]

Result:
q₁ q₂ : ℚ
⊢ {
        num :=
          (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) / ↑((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯,
        reduced := ⋯ }.den ∣
    q₁.den * q₂.den
-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma le_liminf_add (h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
⊢ ∀ y < a + b, ∀ᶠ (a : ι) in f, y < (u + v) a

Tactic:
intro c c_ab

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
⊢ ∀ᶠ (a : ι) in f, c < (u + v) a
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem nat_card : Nat.card (DihedralGroup n) = 2 * n

Proof state:
case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)

Tactic:
rw [Nat.card_eq_fintype_card, card]

Result:
no goals

Proof state:
case zero

⊢ Nat.card (DihedralGroup 0) = 2 * 0

Tactic:
rw [Nat.card_eq_zero_of_infinite]

Result:
no goals

Proof state:
n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n

Tactic:
cases n

Result:
case zero

⊢ Nat.card (DihedralGroup 0) = 2 * 0

case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)
-- Mathlib/Data/Sum/Basic.lean
theorem elim_update_right [DecidableEq α] [DecidableEq β] (f : α → γ) (g : β → γ) (i : β) (c : γ) :
    Sum.elim f (Function.update g i c) = Function.update (Sum.elim f g) (inr i) c

Proof state:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : β
⊢ Sum.elim f (update g x c) (inr x) = update (Sum.elim f g) (inr x) c (inr x)

Tactic:
simp

Result:
no goals

Proof state:
case h.inr
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

Tactic:
by_cases h : x = i

Result:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

case neg
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : ¬x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

Proof state:
case h
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α ⊕ β
⊢ Sum.elim f (update g i c) x = update (Sum.elim f g) (inr i) c x

Tactic:
rcases x with x | x

Result:
case h.inl
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α
⊢ Sum.elim f (update g i c) (inl x) = update (Sum.elim f g) (inr i) c (inl x)

case h.inr
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

Proof state:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

Tactic:
subst h

Result:
case pos
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : β
⊢ Sum.elim f (update g x c) (inr x) = update (Sum.elim f g) (inr x) c (inr x)

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
⊢ Sum.elim f (update g i c) = update (Sum.elim f g) (inr i) c

Tactic:
ext x

Result:
case h
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α ⊕ β
⊢ Sum.elim f (update g i c) x = update (Sum.elim f g) (inr i) c x

Proof state:
case neg
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : ¬x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.inl
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α
⊢ Sum.elim f (update g i c) (inl x) = update (Sum.elim f g) (inr i) c (inl x)

Tactic:
simp

Result:
no goals