harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_subgroup_op (s : Subgroup Gᵐᵒᵖ) : stabilizer G (s : Set Gᵐᵒᵖ) = s.unop

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.unop

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s.unop

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s.unop

Tactic:
have : 1 * MulOpposite.op a ∈ s := (h 1).2 s.one_mem

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
this : 1 * op a ∈ s
⊢ a ∈ s.unop

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ stabilizer G ↑s = s.unop

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.unop

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
this : 1 * op a ∈ s
⊢ a ∈ s.unop

Tactic:
simpa only [op_smul_eq_mul, SetLike.mem_coe, one_mul] using this

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/--
The Schnirelmann density of the set of naturals which are `1 mod m` is `m⁻¹`, for any `m ≠ 1`.

Note that if `m = 1`, this set is empty.
-/
lemma schnirelmannDensity_setOf_mod_eq_one {m : ℕ} (hm : m ≠ 1) :
    schnirelmannDensity {n | n % m = 1} = (m⁻¹ : ℝ)

Proof state:
case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
a b : ℕ
⊢ (fun x => x * m + 1) a = (fun x => x * m + 1) b → a = b

Tactic:
simp [hm'.ne']

Result:
no goals

Proof state:
case inl
hm : 0 ≠ 1
⊢ {n | n % 0 = 1}.Finite

Tactic:
simp

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ n ≤ (n - 1) / m * m + m

Tactic:
have := @Nat.lt_div_mul_add n.pred m hm'

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this✝ : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
this : n.pred < n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m

Proof state:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ y * m ≤ n - Nat.succ 0

Tactic:
exact Nat.mul_le_of_le_div _ _ _ hy'

Result:
no goals

Proof state:
case hab.h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ #(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m)) ≤ 1

Tactic:
simp only [Set.mem_setOf_eq, card_le_one_iff_subset_singleton, subset_iff,
  mem_filter, mem_Ioc, mem_singleton, and_imp]

Result:
case hab.h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∃ x, ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem isPrimitiveRoot_iff' {k : ℕ} [NeZero k] {ζ ξ : Rˣ} (h : IsPrimitiveRoot ζ k) :
    IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Proof state:
case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k

Tactic:
rintro ⟨i, -, hi, rfl⟩

Result:
case mpr.intro.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
case mpr.intro.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi

Result:
no goals

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
constructor

Result:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k

Proof state:
case mp.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
rw [h.pow_iff_coprime <| NeZero.pos k] at hξ

Result:
case mp.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Proof state:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
intro hξ

Result:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Proof state:
case mp.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
exact ⟨i, hik, hξ, rfl⟩

Result:
no goals

Proof state:
case mp
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one

Result:
case mp.intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem MeasureTheory.measure_unitBall_eq_integral_div_gamma {E : Type*} {p : ℝ}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (hp : 0 < p) :
    μ (Metric.ball 0 1) =
      .ofReal ((∫ (x : E), Real.exp (- ‖x‖ ^ p) ∂μ) / Real.Gamma (finrank ℝ E / p + 1))

Proof state:
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : 0 < ↑(finrank ℝ E)
⊢ (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1

Tactic:
simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos,
  Nat.cast_one]

Result:
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : 0 < ↑(finrank ℝ E)
⊢ (∫ (y : ℝ) in Set.Ioi 0, y ^ (↑(finrank ℝ E) - 1) * Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1

Proof state:
case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))

Tactic:
rw [integral_fun_norm_addHaar μ (fun x => Real.exp (- x ^ p)), nsmul_eq_mul, smul_eq_mul,
  mul_div_assoc, mul_div_assoc, mul_comm, mul_assoc, this, mul_one, ofReal_toReal]

Result:
case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) ≠ ⊤

Proof state:
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this : 0 < ↑(finrank ℝ E)
⊢ Real.Gamma (↑(finrank ℝ E) / p) * ↑(finrank ℝ E) = ↑(finrank ℝ E) * Real.Gamma (↑(finrank ℝ E) / p)

Tactic:
ring

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
/-- The minimal positive integer with absolute value smaller than 1 is a prime number. -/
lemma is_prime_of_minimal_nat_zero_lt_and_lt_one : p.Prime

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ False

Tactic:
have hbp : b < a * b := lt_mul_of_one_lt_left (by omega) (by omega)

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
⊢ False

Proof state:
case not_unit
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ¬p = 1

Tactic:
rintro rfl

Result:
case not_unit
f : AbsoluteValue ℚ ℝ
hp0 : 0 < f ↑1
hp1 : f ↑1 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 1 ≤ m
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ 1 < b

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_lt_natDegree {q : S[X]} (hp : p ≠ 0) (hpq : p.degree < q.degree) :
    p.natDegree < q.natDegree

Proof state:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree

Tactic:
exact (not_lt_bot <| hq ▸ hpq).elim

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree

Proof state:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Ici (x : ℝ) : Real.toEReal '' Ici x = Ico ↑x ⊤

Proof state:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Ici x) = Ico ↑x ⊤

Tactic:
rw [WithTop.image_coe_Ici, WithBot.image_coe_Ico]

Result:
x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤

Proof state:
x : ℝ
⊢ Real.toEReal '' Ici x = Ico ↑x ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Ici x) = Ico ↑x ⊤

Proof state:
x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem eq_of_eq_graph {f g : E →ₗ.[R] F} (h : f.graph = g.graph) : f = 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f = g

Tactic:
apply dExt

Result:
case h
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f.domain = g.domain

case h'
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Proof state:
case h'
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
apply (le_of_le_graph h.le).2

Result:
no goals

Proof state:
case h.h
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
x✝ : E
⊢ x✝ ∈ f.domain ↔ x✝ ∈ g.domain

Tactic:
exact mem_domain_iff_of_eq_graph h

Result:
no goals

Proof state:
case h
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f.domain = g.domain

Tactic:
ext

Result:
case h.h
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
f g : E →ₗ.[R] F
h : f.graph = g.graph
x✝ : E
⊢ x✝ ∈ f.domain ↔ x✝ ∈ g.domain
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_eq_take_drop_succ (l : Array α) (i : Nat) (h) : l.eraseIdx i = l.take i ++ l.drop (i + 1)

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l.eraseIdx i h = l.take i ++ l.drop (i + 1)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ { toList := l }.eraseIdx i h = { toList := l }.take i ++ { toList := l }.drop (i + 1)

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ List.drop (i + 1) l = List.take (l.length - (i + 1)) (List.drop (i + 1) l)

Tactic:
rw [List.take_of_length_le]

Result:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ (List.drop (i + 1) l).length ≤ l.length - (i + 1)

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ (List.drop (i + 1) l).length ≤ l.length - (i + 1)

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ { toList := l }.eraseIdx i h✝ = { toList := l }.take i ++ { toList := l }.drop (i + 1)

Tactic:
simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract,
  List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract,
  size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]

Result:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ List.drop (i + 1) l = List.take (l.length - (i + 1)) (List.drop (i + 1) l)

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ { toList := l }.eraseIdx i h = { toList := l }.take i ++ { toList := l }.drop (i + 1)

Tactic:
simp only [size_toArray] at h

Result:
case mk
α : Type u_1
i : Nat
l : List α
h✝ : i < { toList := l }.size
h : i < l.length
⊢ { toList := l }.eraseIdx i h✝ = { toList := l }.take i ++ { toList := l }.drop (i + 1)
-- Mathlib/Data/List/ModifyLast.lean
theorem modifyLast_append_of_right_ne_nil (f : α → α) (l₁ l₂ : List α) (_ : l₂ ≠ []) :
    modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Proof state:
case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
exact modifyLast_concat _ hd _

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
l₁ : List α
x✝ : [] ≠ []
⊢ modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
all_goals { exact cons_ne_nil _ _ }

Result:
no goals

Proof state:
α : Type u_1
f : α → α
l₁ l₂ : List α
x✝ : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Tactic:
cases l₂ with
| nil => contradiction
| cons hd tl =>
  cases tl with
  | nil => exact modifyLast_concat _ hd _
  | cons hd' tl' =>
    rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
      modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
      modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
      append_assoc]
    all_goals { exact cons_ne_nil _ _ }

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')

Tactic:
rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
  modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
  modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
  append_assoc]

Result:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Proof state:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
exact cons_ne_nil _ _

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
x✝ : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)

Tactic:
cases tl with
| nil => exact modifyLast_concat _ hd _
| cons hd' tl' =>
  rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
    modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
    modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
    append_assoc]
  all_goals { exact cons_ne_nil _ _ }

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
    a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a

Tactic:
refine ⟨fun h => ?_, fun ⟨m, h⟩ => (h.cons a).trans (perm_cons_erase m).symm⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : a :: l₁ ~ l₂
⊢ a ∈ l₂ ∧ l₁ ~ l₂.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : a :: l₁ ~ l₂
this : a ∈ l₂
⊢ a ∈ l₂ ∧ l₁ ~ l₂.erase a

Tactic:
exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : a :: l₁ ~ l₂
⊢ a ∈ l₂ ∧ l₁ ~ l₂.erase a

Tactic:
have : a ∈ l₂ := h.subset (mem_cons_self a l₁)

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : a :: l₁ ~ l₂
this : a ∈ l₂
⊢ a ∈ l₂ ∧ l₁ ~ l₂.erase a
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_eq_zero_iff_ne_and_wbtw {p₁ p₂ p₃ : P} :
    ∠ p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Proof state:
case mp.intro.intro.intro.inr.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0

Tactic:
exact ⟨hr0.ne.symm, hp₁p₂⟩

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1

Tactic:
simp only [ne_eq, not_forall, exists_prop]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_comp_reindex_eq (f : Π i, s i →ₗ[R] t i) (e : ι ≃ ι₂) :
    map (fun i ↦ f (e.symm i)) ∘ₗ reindex R s e = reindex R t e ∘ₗ map f

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
⊢ (map fun i => f (e.symm i)) ∘ₗ ↑(reindex R s e) = ↑(reindex R t e) ∘ₗ map f

Tactic:
ext m

Result:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι) → s i
⊢ (((map fun i => f (e.symm i)) ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e) ∘ₗ map f).compMultilinearMap (tprod R)) m

Proof state:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
m : (i : ι) → s i
⊢ (((map fun i => f (e.symm i)) ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) m =
    ((↑(reindex R t e) ∘ₗ map f).compMultilinearMap (tprod R)) m

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
  LinearMap.comp_apply, reindex_tprod, map_tprod]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem iff_of_openCover (𝒰 : Y.OpenCover) [∀ i, IsAffine (𝒰.obj i)] :
    P f ↔ ∀ i, Q (𝒰.pullbackHom f i)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ (∀ (i : 𝒰.J), Q (f ∣_ ↑⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩)) ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
exact forall_congr' fun i ↦ Q.arrow_mk_iso_iff
  (morphismRestrictOpensRange f _)

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
rw [iff_of_iSup_eq_top (P := P)
  (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ (∀ (i : 𝒰.J), Q (f ∣_ ↑⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩)) ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ P f ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
letI := isLocal_affineProperty P

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)