harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_self (μ : Measure α) [SigmaFinite μ] : μ.rnDeriv μ =ᵐ[μ] fun _ ↦ 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Tactic:
rwa [withDensity_eq_iff_of_sigmaFinite (measurable_rnDeriv _ _).aemeasurable] at h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ AEMeasurable 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Tactic:
conv_rhs at h => rw [h_one]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Tactic:
have h_one : μ = μ.withDensity 1 := by simp

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ = μ.withDensity 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Tactic:
rw [singularPart_self, add_zero] at h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ AEMeasurable 1 μ

Tactic:
exact aemeasurable_const

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1

Tactic:
have h := rnDeriv_add_singularPart μ μ

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun x => 1
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem range_pow_padicValNat_subset_divisors {n : ℕ} (hn : n ≠ 0) :
    (Finset.range (padicValNat p n + 1)).image (p ^ ·) ⊆ n.divisors

Proof state:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ k ≤ padicValNat p n

Tactic:
omega

Result:
no goals

Proof state:
p n : ℕ
hn : n ≠ 0
⊢ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ n.divisors

Tactic:
intro t ht

Result:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ n.divisors

Proof state:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n + 1, p ^ a = t
⊢ t ∈ n.divisors

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Result:
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ n.divisors

Proof state:
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0

Tactic:
exact ⟨(pow_dvd_pow p <| by omega).trans pow_padicValNat_dvd, hn⟩

Result:
no goals

Proof state:
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ n.divisors

Tactic:
rw [Nat.mem_divisors]

Result:
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0

Proof state:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ n.divisors

Tactic:
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht

Result:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n + 1, p ^ a = t
⊢ t ∈ n.divisors
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem zeta_sub_one_prime' [h : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    Prime ((hζ.toInteger - 1))

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ?m.223281 ↑(?m.223267 ^ (0 + 1))

Tactic:
simpa only [zero_add, pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa only [zero_add, pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ Prime (hζ.toInteger - 1)

Tactic:
convert zeta_sub_one_prime (k := 0) (by simpa only [zero_add, pow_one])

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).support = p.support

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).support = p.support

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).support = p.support

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).support = p.support
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem sqrtTwoAddSeries_step_up (c d : ℕ) {a b n : ℕ} {z : ℝ} (hz : sqrtTwoAddSeries (c / d) n ≤ z)
    (hb : 0 < b) (hd : 0 < d) (h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b) :
    sqrtTwoAddSeries (a / b) (n + 1) ≤ z

Proof state:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
rw [sqrtTwoAddSeries_succ]

Result:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n

Proof state:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Tactic:
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd

Result:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Proof state:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z

Tactic:
refine le_trans ?_ hz

Result:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n

Proof state:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b

Tactic:
exact mod_cast h

Result:
no goals

Proof state:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Tactic:
rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow,
  add_div_eq_mul_add_div _ _ (ne_of_gt hb'), div_le_div_iff₀ hb' (pow_pos hd' _)]

Result:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b

Proof state:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Tactic:
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb

Result:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Proof state:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
apply sqrtTwoAddSeries_monotone_left

Result:
case h
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d
-- 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 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
⊢ 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 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:
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:
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
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_pow_eq_one 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/RingTheory/TensorProduct/Basic.lean
theorem mul'_comp_tensorTensorTensorComm :
    LinearMap.mul' R (A ⊗[R] B) ∘ₗ tensorTensorTensorComm R A A B B =
      map (LinearMap.mul' R A) (LinearMap.mul' R B)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ LinearMap.mul' R (A ⊗[R] B) ∘ₗ ↑(tensorTensorTensorComm R A A B B) = map (LinearMap.mul' R A) (LinearMap.mul' R B)

Tactic:
ext

Result:
case a.a.h.h.a.h.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝³ x✝² : A
x✝¹ x✝ : B
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry (LinearMap.mul' R (A ⊗[R] B) ∘ₗ ↑(tensorTensorTensorComm R A A B B))))
              x✝³)
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B)))) x✝³)
            x✝²))
        x✝¹)
      x✝

Proof state:
case a.a.h.h.a.h.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝³ x✝² : A
x✝¹ x✝ : B
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry (LinearMap.mul' R (A ⊗[R] B) ∘ₗ ↑(tensorTensorTensorComm R A A B B))))
              x✝³)
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B)))) x✝³)
            x✝²))
        x✝¹)
      x✝

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Invariant.lean
theorem fixed_of_fixed1_aux1 [DecidableEq (Ideal B)] :
    ∃ a b : B, (∀ g : G, g • a = a) ∧ a ∉ Q ∧
    ∀ g : G, algebraMap B (B ⧸ Q) (g • b) = algebraMap B (B ⧸ Q) (if g • Q = Q then a else 0)

Proof state:
B : Type u_2
inst✝⁵ : CommRing B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
Q : Ideal B
inst✝¹ : Q.IsPrime
inst✝ : DecidableEq (Ideal B)
val✝ : Fintype G
P : Ideal B := (Finset.filter (fun g => g • Q ≠ Q) Finset.univ).inf fun g => g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) f) = (algebraMap B (B ⧸ Q)) 0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0

Tactic:
rwa [map_zero, hq, ← hr, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_X,
  mul_eq_zero, or_iff_right (pow_ne_zero _ hbQ)] at hf

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_zero_pos (R) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R]
    {k : ℕ} (h_pos: 0 < k) : choose (0 : R) k = 0

Proof state:
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
h_pos : 0 < k
⊢ choose 0 k = 0

Tactic:
rw [← Nat.succ_pred_eq_of_pos h_pos, choose_zero_succ]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma pairingIn_reflection_perm_self_right [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S i (P.reflection_perm j j) = - P.pairingIn S i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i j : ι
⊢ P.pairingIn S i ((P.reflection_perm j) j) = -P.pairingIn S i j

Tactic:
simp [← (FaithfulSMul.algebraMap_injective S R).eq_iff]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem eq_iff_atom_le_iff {α} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
    x = y ↔ ∀ a, IsAtom a → (a ≤ x ↔ a ≤ y)

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

Tactic:
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩

Result:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
⊢ x = y

Tactic:
exact le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx)
  (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds (hdf : ∀ᶠ x in 𝓝 a, DifferentiableAt ℝ f x)
    (hg' : ∀ᶠ x in 𝓝 a, deriv g x ≠ 0) (hfa : Tendsto f (𝓝 a) (𝓝 0)) (hga : Tendsto g (𝓝 a) (𝓝 0))
    (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝 a) l) :
    Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Tactic:
apply lhopital_zero_nhds' <;>
  (first | apply eventually_nhdsWithin_of_eventually_nhds |
    apply tendsto_nhdsWithin_of_tendsto_nhds) <;> assumption

Result:
no goals

Proof state:
case hdiv
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x => deriv f x / deriv g x) (𝓝[≠] a) l

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Result:
case hdiv.h
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l

Proof state:
case hg'
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Result:
case hg'.h
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0

Proof state:
case hdiv
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x => deriv f x / deriv g x) (𝓝[≠] a) l

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
 apply tendsto_nhdsWithin_of_tendsto_nhds

Result:
case hdiv.h
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyInf_eq_iSup_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)}
    (h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
    coverEntropyInf T F = ⨆ (i : ι) (_ : p i), coverEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
rcases (HasBasis.mem_iff h).1 U_uni with ⟨i, h_i, si_U⟩

Result:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
  (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Result:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Proof state:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
exact (coverEntropyInfEntourage_antitone T F si_U).trans
  (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_right_eq_arcsin_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₂ p₃ p₁ = Real.arcsin (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₁ = ↑(Real.arcsin (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₁ = ↑(Real.arcsin (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₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arcsin_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals