harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
  sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
  dist_comm p₁ p₃]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem finite_setOf_absNorm_le [CharZero S] (n : ℕ) :
    {I : Ideal S | Ideal.absNorm I ≤ n}.Finite

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I ≤ n} = ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}

Tactic:
ext

Result:
case h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
x✝ : Ideal S
⊢ x✝ ∈ {I | absNorm I ≤ n} ↔ x✝ ∈ ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ (⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}).Finite

Tactic:
refine Set.Finite.biUnion (Set.finite_Icc 0 n) (fun i _ => Ideal.finite_setOf_absNorm_eq i)

Result:
no goals

Proof state:
case h
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
x✝ : Ideal S
⊢ x✝ ∈ {I | absNorm I ≤ n} ↔ x✝ ∈ ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}

Tactic:
simp

Result:
no goals

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I ≤ n}.Finite

Tactic:
rw [show {I : Ideal S | Ideal.absNorm I ≤ n} =
  (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | Ideal.absNorm I = i}) by ext; simp]

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ (⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}).Finite
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem finMulAntidiag_eq_piFinset_divisors_filter {d m n : ℕ} (hmn : m ∣ n) (hn : n ≠ 0) :
    finMulAntidiag d m =
      {f ∈ Fintype.piFinset fun _ : Fin d => n.divisors | ∏ i, f i = m}

Proof state:
case h
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)

Tactic:
simp only [mem_univ, not_true, IsEmpty.forall_iff, implies_true, ne_eq, true_and,
  Fintype.mem_piFinset, mem_divisors, Nat.isUnit_iff, mem_filter]

Result:
case h
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Proof state:
case h
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Tactic:
constructor

Result:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

case h.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m

Proof state:
case h.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0

Tactic:
exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩

Result:
no goals

Proof state:
case h.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m

Tactic:
rw [mem_finMulAntidiag]

Result:
case h.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0

Proof state:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Tactic:
intro hf

Result:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Proof state:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0

Tactic:
exact fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩

Result:
no goals

Proof state:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Tactic:
refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩

Result:
case h.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0

Proof state:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiag m = filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)

Tactic:
ext f

Result:
case h
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem factors_normalizedMooreComplex_PInfty (n : ℕ) :
    Subobject.Factors (NormalizedMooreComplex.objX X n) (PInfty.f n)

Proof state:
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors (PInfty.f (n + 1))

Tactic:
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]

Result:
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ i ∈ Finset.univ, (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))

Proof state:
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ i ∈ Finset.univ, (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))

Tactic:
intro i _

Result:
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X n).Factors (PInfty.f n)

Tactic:
rcases n with _|n

Result:
case zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (NormalizedMooreComplex.objX X 0).Factors (PInfty.f 0)

case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).Factors (PInfty.f (n + 1))

Proof state:
case zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (NormalizedMooreComplex.objX X 0).Factors (PInfty.f 0)

Tactic:
apply top_factors

Result:
no goals

Proof state:
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))

Tactic:
apply kernelSubobject_factors

Result:
case succ.w
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ (P (n + 1)).f (n + 1) ≫ X.δ i.succ = 0

Proof state:
case succ.w
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ (P (n + 1)).f (n + 1) ≫ X.δ i.succ = 0

Tactic:
exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
theorem existsUnique_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) :
    ∃! e' : R, IsIdempotentElem e' ∧ f e' = e

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃! e', IsIdempotentElem e' ∧ f e' = e

Tactic:
obtain ⟨e', he₂, rfl⟩ := exists_isIdempotentElem_eq_of_ker_isNilpotent f h e he he'

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
⊢ ∃! e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e'

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
⊢ ∃! e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e'

Tactic:
exact ⟨e', ⟨he₂, rfl⟩, fun x ⟨hx, hx'⟩ ↦
  eq_of_isNilpotent_sub_of_isIdempotentElem hx he₂
    (h _ (by rw [RingHom.mem_ker, map_sub, hx', sub_self]))⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 => IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ x - e' ∈ RingHom.ker f

Tactic:
rw [RingHom.mem_ker, map_sub, hx', sub_self]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma dvd_iff_div_mul_eq (n d : ℕ) : d ∣ n ↔ n / d * d = n :=
  ⟨fun h => Nat.div_mul_cancel h, fun h => by rw [← h]; exact Nat.dvd_mul_left _ _⟩

Proof state:
n d : ℕ
h : n / d * d = n
⊢ d ∣ n / d * d

Tactic:
exact Nat.dvd_mul_left _ _

Result:
no goals

Proof state:
n d : ℕ
h : n / d * d = n
⊢ d ∣ n

Tactic:
rw [← h]

Result:
n d : ℕ
h : n / d * d = n
⊢ d ∣ n / d * d
-- Mathlib/NumberTheory/Rayleigh.lean
theorem Irrational.beattySeq'_pos_eq {r : ℝ} (hr : Irrational r) :
    {beattySeq' r k | k > 0} = {beattySeq r k | k > 0}

Proof state:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ↑⌊↑k * r⌋ < ↑k * r ∧ ↑k * r ≤ ↑⌊↑k * r⌋ + 1

Tactic:
refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩

Result:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
h : ↑⌊↑k * r⌋ = ↑k * r
⊢ False

Proof state:
r : ℝ
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}

Tactic:
dsimp only [beattySeq, beattySeq']

Result:
r : ℝ
hr : Irrational r
⊢ {x | ∃ k > 0, ⌈↑k * r⌉ - 1 = x} = {x | ∃ k > 0, ⌊↑k * r⌋ = x}

Proof state:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ - 1 = x✝ ↔ ⌊↑k * r⌋ = x✝

Tactic:
congr!

Result:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ - 1 = ⌊↑k * r⌋

Proof state:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝¹ x✝ : ℤ
⊢ x✝ > 0 ∧ ⌈↑x✝ * r⌉ - 1 = x✝¹ ↔ x✝ > 0 ∧ ⌊↑x✝ * r⌋ = x✝¹

Tactic:
rename_i k

Result:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 ∧ ⌈↑k * r⌉ - 1 = x✝ ↔ k > 0 ∧ ⌊↑k * r⌋ = x✝

Proof state:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 ∧ ⌈↑k * r⌉ - 1 = x✝ ↔ k > 0 ∧ ⌊↑k * r⌋ = x✝

Tactic:
rw [and_congr_right_iff]

Result:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 → (⌈↑k * r⌉ - 1 = x✝ ↔ ⌊↑k * r⌋ = x✝)

Proof state:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
h : ↑⌊↑k * r⌋ = ↑k * r
⊢ False

Tactic:
exact (hr.int_mul hk.ne').ne_int ⌊k * r⌋ h.symm

Result:
no goals

Proof state:
r : ℝ
hr : Irrational r
⊢ {x | ∃ k > 0, ⌈↑k * r⌉ - 1 = x} = {x | ∃ k > 0, ⌊↑k * r⌋ = x}

Tactic:
congr! 4

Result:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝¹ x✝ : ℤ
⊢ x✝ > 0 ∧ ⌈↑x✝ * r⌉ - 1 = x✝¹ ↔ x✝ > 0 ∧ ⌊↑x✝ * r⌋ = x✝¹

Proof state:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 → (⌈↑k * r⌉ - 1 = x✝ ↔ ⌊↑k * r⌋ = x✝)

Tactic:
intro hk

Result:
case h.e'_2.h.h.e'_2.h.a
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ - 1 = x✝ ↔ ⌊↑k * r⌋ = x✝

Proof state:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ - 1 = ⌊↑k * r⌋

Tactic:
rw [sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, add_sub_cancel_right]

Result:
case h.e'_2.h.h.e'_2.h.a.a.h.e'_2
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ↑⌊↑k * r⌋ < ↑k * r ∧ ↑k * r ≤ ↑⌊↑k * r⌋ + 1
-- Mathlib/Data/Finsupp/Single.lean
theorem support_update_subset [DecidableEq α] :
    support (f.update a b) ⊆ insert a f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ (if b = 0 then f.support.erase a else insert a f.support) ⊆ insert a f.support

Tactic:
split_ifs

Result:
case pos
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h✝ : b = 0
⊢ f.support.erase a ⊆ insert a f.support

case neg
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h✝ : ¬b = 0
⊢ insert a f.support ⊆ insert a f.support

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h✝ : b = 0
⊢ f.support.erase a ⊆ insert a f.support

Tactic:
exact (erase_subset _ _).trans (subset_insert _ _)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ (f.update a b).support ⊆ insert a f.support

Tactic:
rw [support_update]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
⊢ (if b = 0 then f.support.erase a else insert a f.support) ⊆ insert a f.support

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
inst✝ : DecidableEq α
h✝ : ¬b = 0
⊢ insert a f.support ⊆ insert a f.support

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Scheme.zeroLocus_inf (X : Scheme.{u}) {U : X.Opens} (I J : Ideal Γ(X, U)) :
    X.zeroLocus (U := U) ↑(I ⊓ J) = X.zeroLocus (U := U) I ∪ X.zeroLocus (U := U) J

Proof state:
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)

Tactic:
simp only [← U.toSpecΓ_preimage_zeroLocus, PrimeSpectrum.zeroLocus_inf I J,
  Set.preimage_union]

Result:
no goals

Proof state:
case neg
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
hxU : x ∉ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
simp only [Submodule.inf_coe, Set.mem_union,
  codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
  codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]

Result:
no goals

Proof state:
case pos
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
⊢ X.zeroLocus ↑(I ⊓ J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
ext x

Result:
case h
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Proof state:
case h
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
by_cases hxU : x ∈ U

Result:
case pos
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

case neg
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↑↑X.toPresheafedSpace
hxU : x ∉ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J
-- Mathlib/Data/Multiset/Sym.lean
theorem card_sym2 {m : Multiset α} :
    Multiset.card m.sym2 = Nat.choose (Multiset.card m + 1) 2

Proof state:
α : Type u_1
m : Multiset α
⊢ m.sym2.card = (m.card + 1).choose 2

Tactic:
refine m.inductionOn fun xs => ?_

Result:
α : Type u_1
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2

Proof state:
α : Type u_1
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2

Tactic:
simp [List.length_sym2]

Result:
no goals
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem ncoeff_of_coeff (f : ℤ → Module.End R V)
    (hf : ∀(x : V), ∃(n : ℤ), ∀(m : ℤ), m < n → (f m) x = 0) (n : ℤ) :
    (of_coeff f hf) [[n]] = f (-n - 1)

Proof state:
case h
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0
n : ℤ
v : V
⊢ (of_coeff f hf[[n]]) v = (f (-n - 1)) v

Tactic:
rw [ncoeff, coeff_apply, of_coeff_apply_coeff]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0
n : ℤ
⊢ of_coeff f hf[[n]] = f (-n - 1)

Tactic:
ext v

Result:
case h
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0
n : ℤ
v : V
⊢ (of_coeff f hf[[n]]) v = (f (-n - 1)) v
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotientEquivQuotientMinpolyMap_apply_mk (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
    pb.quotientEquivQuotientMinpolyMap I (Ideal.Quotient.mk (I.map (algebraMap R S))
      (aeval pb.gen g)) = Ideal.Quotient.mk
        (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
          (g.map (Ideal.Quotient.mk I))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ (pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply,
  quotientEquiv_mk, AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval,
  AdjoinRoot.aeval_eq, AdjoinRoot.quotEquivQuotMap_apply_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d {f : E → ℝ} {f' : E →L[ℝ] ℝ}
    (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀)
    (hφ' : HasStrictFDerivAt φ φ' x₀) : ∃ a b : ℝ, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0

Proof state:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
⊢ ∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0

Tactic:
refine ⟨Λ 1, Λ₀, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
⊢ (Λ 1, Λ₀) ≠ 0

case intro.intro.intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
⊢ Λ 1 • f' + Λ₀ • φ' = 0

Proof state:
case intro.intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
hΛ : Λ 1 = 0 ∧ Λ₀ = 0
⊢ Λ = 0 ∧ Λ₀ = 0

Tactic:
refine ⟨LinearMap.ext fun x => ?_, hΛ.2⟩

Result:
case intro.intro.intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
hΛ : Λ 1 = 0 ∧ Λ₀ = 0
x : ℝ
⊢ Λ x = 0 x
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph_toLinearPMap {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0)
    (x : g.map (LinearMap.fst R E F)) : (x.val, g.toLinearPMap x) ∈ g

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑x, valFromGraph hg ⋯) ∈ g

Tactic:
exact valFromGraph_mem hg x.2

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑x, ↑g.toLinearPMap x) ∈ g

Tactic:
rw [toLinearPMap_apply_aux hg]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑x, valFromGraph hg ⋯) ∈ g