harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem pell_eq (n : ℕ) : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 :=
  let pn := pell_eqz a1 n
  have h : (↑(xn a1 n * xn a1 n) : ℤ) - ↑(d a1 * yn a1 n * yn a1 n) = 1

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
h : ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1
hl : Pell.d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ ↑(xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n) = ↑1

Tactic:
rw [Int.ofNat_sub hl]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
h : ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1
hl : Pell.d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = ↑1

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n) * ↑(xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1

Tactic:
exact pn

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
h : ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1
hl : Pell.d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = ↑1

Tactic:
exact h

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1

Tactic:
rw [Int.ofNat_mul]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n) * ↑(xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1

Tactic:
repeat' rw [Int.ofNat_mul]; exact pn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n !

Proof state:
n : ℕ
⊢ Gamma (↑n + 1) = ↑n !

Tactic:
rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
  Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
lemma LinearIndependent.pair_symm_iff {x y : M} :
    LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
specialize h t s

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ ∀ (x y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
intro x y h s t

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]

Tactic:
simp only [LinearIndependent.pair_iff]

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ ∀ (x y : M), (∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
rwa [add_comm, and_comm]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
suffices ∀ x y : M, LinearIndependent R ![x, y] → LinearIndependent R ![y, x] by tauto

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem map_div_of_coprime [CommGroupWithZero R] {f : ArithmeticFunction R}
    (hf : IsMultiplicative f) {l d : ℕ} (hdl : d ∣ l) (hl : (l/d).Coprime d) (hd : f d ≠ 0) :
    f (l / d) = f l / f d

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f l = f (l / d) * f d

Tactic:
rw [← hf.right hl, Nat.div_mul_cancel hdl]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f (l / d) = f l / f d

Tactic:
apply (div_eq_of_eq_mul hd ..).symm

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f l = f (l / d) * f d
-- Mathlib/Data/List/Infix.lean
theorem concat_get_prefix {x y : List α} (h : x <+: y) (hl : x.length < y.length) :
    x ++ [y.get ⟨x.length, hl⟩] <+: y

Proof state:
case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y

Tactic:
nth_rw 1 [List.prefix_iff_eq_take.mp h]

Result:
case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y

Proof state:
case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y

Tactic:
convert List.take_append_drop (x.length + 1) y using 2

Result:
case h.e'_2.h.e'_5
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take (x.length + 1) y

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

case h.e'_2.h.e'_5.h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take (x.length + 1) y

Tactic:
rw [← List.take_concat_get, List.concat_eq_append]

Result:
case h.e'_2.h.e'_5
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

case h.e'_2.h.e'_5.h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length

Proof state:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get ⟨x.length, hl⟩] <+: y

Tactic:
use y.drop (x.length + 1)

Result:
case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) :
    k.descFactorial n ≤ m.descFactorial n

Proof state:
n k m : ℕ
h : k ≤ m
⊢ k.descFactorial n ≤ m.descFactorial n

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [descFactorial_succ, descFactorial_succ]
  exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Result:
no goals

Proof state:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n

Tactic:
exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

Result:
no goals

Proof state:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)

Tactic:
rw [descFactorial_succ, descFactorial_succ]

Result:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n

Proof state:
case zero
k m : ℕ
h : k ≤ m
⊢ k.descFactorial 0 ≤ m.descFactorial 0

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem subset_piiUnionInter {π : ι → Set (Set α)} {S : Set ι} {i : ι} (his : i ∈ S) :
    π i ⊆ piiUnionInter π S

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}

Tactic:
exact subset_union_left

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ {i} ⊆ S

Tactic:
intro j hj

Result:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j ∈ {i}
⊢ j ∈ S

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ π i ⊆ piiUnionInter π S

Tactic:
have h_ss : {i} ⊆ S := by
  intro j hj
  rw [mem_singleton_iff] at hj
  rwa [hj]

Result:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}

Tactic:
rw [piiUnionInter_singleton]

Result:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S

Tactic:
refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)

Result:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j ∈ {i}
⊢ j ∈ S

Tactic:
rw [mem_singleton_iff] at hj

Result:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
⊢ j ∈ S

Proof state:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
⊢ j ∈ S

Tactic:
rwa [hj]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive (attr := simp)]
lemma stabilizer_smul_eq_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β)
    (h : Injective (· • b : α → β)) : stabilizer G (a • b) = stabilizer G a

Proof state:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
h : Injective fun x => x • b
⊢ stabilizer G (a • b) = stabilizer G a

Tactic:
refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_

Result:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
h : Injective fun x => x • b
a : G
ha : a ∈ stabilizer G (a✝ • b)
⊢ a ∈ stabilizer G a✝

Proof state:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
h : Injective fun x => x • b
a : G
ha : a ∈ stabilizer G (a✝ • b)
⊢ a ∈ stabilizer G a✝

Tactic:
simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem dim_le_degree_of_root (h : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0)
    (root : aeval h.gen p = 0) : ↑h.dim ≤ p.degree

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval h.gen) p = 0
⊢ ↑h.dim ≤ p.degree

Tactic:
rw [degree_eq_natDegree ne_zero]

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval h.gen) p = 0
⊢ ↑h.dim ≤ ↑p.natDegree

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval h.gen) p = 0
⊢ ↑h.dim ≤ ↑p.natDegree

Tactic:
exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma XYIdeal_eq₂ {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁)
    (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
    XYIdeal W x₂ (C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ XYIdeal W x₂ (C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
nth_rw 1 [hy₂]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ XYIdeal W x₂ (C (eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))) =
    XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Iic (x : ℝ) : Real.toEReal '' Iic x = Ioc ⊥ ↑x

Proof state:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Iic x) = Ioc ⊥ ↑x

Tactic:
rw [WithTop.image_coe_Iic, WithBot.image_coe_Iic]

Result:
x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x

Proof state:
x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x

Tactic:
rfl

Result:
no goals

Proof state:
x : ℝ
⊢ Real.toEReal '' Iic x = Ioc ⊥ ↑x

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

Result:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Iic x) = Ioc ⊥ ↑x
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).FG) : (⊤ : Subalgebra R A).FG :=
  let ⟨s, hs⟩ := h
  ⟨s, toSubmodule.injective <| by
    rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
    exact Algebra.subset_adjoin⟩

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(toSubmodule (Algebra.adjoin R ↑s))

Tactic:
exact Algebra.subset_adjoin

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ toSubmodule (Algebra.adjoin R ↑s) = toSubmodule ⊤

Tactic:
rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(toSubmodule (Algebra.adjoin R ↑s))
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_const_one (c : E) (l : Filter α) :
    IsBigOWith ‖c‖ l (fun _x : α => c) fun _x => (1 : F)

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
inst✝¹ : One F
inst✝ : NormOneClass F
c : E
l : Filter α
⊢ IsBigOWith ‖c‖ l (fun _x => c) fun _x => 1

Tactic:
simp [isBigOWith_iff]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_val_preimage_restrictPreimage {u : Set t} :
    Subtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u)

Proof state:
case h
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
x✝ : α
⊢ x✝ ∈ Subtype.val '' (t.restrictPreimage f ⁻¹' u) ↔ x✝ ∈ f ⁻¹' (Subtype.val '' u)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ Subtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
x✝ : α
⊢ x✝ ∈ Subtype.val '' (t.restrictPreimage f ⁻¹' u) ↔ x✝ ∈ f ⁻¹' (Subtype.val '' u)
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_of_mul_apply (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) {x : R}
    (hx : ∀ y : R, f (x * y) = f x * f y) : seminormFromBounded' f x = f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x✝ : R
hx✝ : ∀ (y : R), f (x✝ * y) = f x✝ * f y
x : R
hx : ¬f x = 0
⊢ f x✝ * (f x / f x) ≤ f x✝

Tactic:
rw [div_self hx, mul_one]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
⊢ (fun y => f x * (f y / f y)) y ≤ f x

Tactic:
simp only [hy0, div_zero, mul_zero]

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
⊢ 0 ≤ f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ BddAbove (Set.range fun y => f x * (f y / f y))

Tactic:
use f x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ f x ∈ upperBounds (Set.range fun y => f x * (f y / f y))

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : ¬f y = 0
⊢ (fun y => f x * (f y / f y)) y ≤ f x

Tactic:
simp only [div_self hy0, mul_one, le_refl]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem _root_.LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot (N : LieSubmodule R L M) :
    LieModule.IsNilpotent L N ↔ ∃ k, N.lcs k = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L (↥N) k = ⊥ ↔ LieSubmodule.lcs k N = ⊥

Tactic:
rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
  inf_eq_right.mpr (N.lcs_le_self k)]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L (↥N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥

Tactic:
refine exists_congr fun k => ?_

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L (↥N) k = ⊥ ↔ LieSubmodule.lcs k N = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
⊢ IsNilpotent L ↥N ↔ ∃ k, LieSubmodule.lcs k N = ⊥

Tactic:
rw [isNilpotent_iff R L N]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L (↥N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
-- Mathlib/RingTheory/RingHom/Flat.lean
lemma respectsIso : RespectsIso Flat

Proof state:
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] => Flat

Tactic:
apply stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Flat

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.Flat

Tactic:
exact of_bijective e.bijective

Result:
no goals

Proof state:
⊢ ∀ {R S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Flat

Tactic:
introv

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.Flat
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_rel {l : Array α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b)

Proof state:
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a { toList := l }) (foldr (fun a acc => g a acc) b { toList := l })

Proof state:
case mk
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a { toList := l }) (foldr (fun a acc => g a acc) b { toList := l })

Tactic:
simpa using List.foldr_rel r h (by simpa using h')

Result:
no goals