harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_braidWord_eq (i i' : B) :
    π (braidWord M i i') = π (braidWord M i' i)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
have := cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' (M i i')
  (Nat.le_mul_of_pos_right _ (by norm_num))

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
nth_rw 2 [M.symmetric i i'] at this

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
exact this

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
rw [tsub_eq_of_eq_add (mul_two (M i i'))] at this

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem dist_le_zero {x y : γ} : dist x y ≤ 0 ↔ x = y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y

Tactic:
simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_iff_right :
    a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
  (Equiv.addRight m).symm.exists_congr_left.trans <| by simp [add_sub_add_comm, hm, add_smul, ModEq]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a₁ a₂ b₁ b₂ : α
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = (Equiv.symm (Equiv.addRight m)).symm b • p) ↔ a₁ ≡ b₁ [PMOD p]

Tactic:
simp [add_sub_add_comm, hm, add_smul, ModEq]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem prime_C_iff : Prime (C r) ↔ Prime r :=
  ⟨comap_prime C (evalRingHom (0 : R)) fun _ => eval_C, fun hr => by
    have := hr.1
    rw [← Ideal.span_singleton_prime] at hr ⊢
    · rw [← Set.image_singleton, ← Ideal.map_span]
      apply Ideal.isPrime_map_C_of_isPrime hr
    · intro h; apply (this (C_eq_zero.mp h))
    · assumption⟩

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (C r)

Tactic:
rw [← Ideal.span_singleton_prime] at hr ⊢

Result:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

Tactic:
intro h

Result:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
h : C r = 0
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

Tactic:
rw [← Set.image_singleton, ← Ideal.map_span]

Result:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
h : C r = 0
⊢ False

Tactic:
apply (this (C_eq_zero.mp h))

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
⊢ Prime (C r)

Tactic:
have := hr.1

Result:
R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (C r)

Proof state:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime

Tactic:
apply Ideal.isPrime_map_C_of_isPrime hr

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`,
`|X| ^ n * exp (v * X)` is integrable. -/
lemma integrable_pow_abs_mul_exp_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n * exp (v * X ω)) μ

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
⊢ Integrable (fun ω => |X ω| ^ n * rexp (v * X ω)) μ

Tactic:
convert integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean
lemma Ideal.map_mk_comap_factorPow {a b : ℕ} (apos : 0 < a) (le : a ≤ b) :
    (I.map (mk (I ^ a))).comap (factorPow I le) = I.map (mk (I ^ b))

Proof state:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ comap (factorPow I le) (map (mk (I ^ a)) I) = map (mk (I ^ b)) I

Tactic:
apply Ideal.map_mk_comap_factor

Result:
case hIJ
R : Type u_3
inst✝ : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ I ^ a ≤ I

Proof state:
case hIJ
R : Type u_3
inst✝ : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ I ^ a ≤ I

Tactic:
exact pow_le_self (Nat.not_eq_zero_of_lt apos)

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem card_of_finset' {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) [Fintype p] :
    Fintype.card p = #s

Proof state:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = #s

Tactic:
rw [← card_ofFinset s H]

Result:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
theorem Complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) :
    (∑' n : ℤ, cexp (-π * a * (n : ℂ) ^ 2)) =
      1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n : ℂ) ^ 2)

Proof state:
a : ℂ
ha : 0 < a.re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)

Tactic:
simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
funext a d

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d

Proof state:
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Tactic:
exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d

Tactic:
apply propext

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d

Tactic:
constructor

Result:
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d

case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Proof state:
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d

Tactic:
exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_mul_cancel' (f g₁ g₂ : R) (U hu₁ hu₂) :
    const R g₁ g₂ U hu₂ * const R f g₁ U hu₁ = const R f g₂ U hu₂

Proof state:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl
⊢ const R g₁ g₂ U hu₂ * const R f g₁ U hu₁ = const R f g₂ U hu₂

Tactic:
rw [mul_comm, const_mul_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_one {f : End R M} {μ : R} :
    f.genEigenspace μ 1 = LinearMap.ker (f - μ • 1)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) 1 = LinearMap.ker (f - μ • 1)

Tactic:
rw [← Nat.cast_one, genEigenspace_nat, pow_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.coe_re_apply_self {A : Matrix n n α} (h : A.IsHermitian) (i : n) :
    (re (A i i) : α) = A i i

Proof state:
α : Type u_1
n : Type u_4
inst✝ : RCLike α
A : Matrix n n α
h : A.IsHermitian
i : n
⊢ ↑(re (A i i)) = A i i

Tactic:
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem lift_apply_inl (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r)
    (r : R) :
    lift f g hg hfg hgf (inl r) = f r :=
  show f r + g 0 = f r by rw [map_zero, add_zero]

Proof state:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r : R
⊢ f r + g 0 = f r

Tactic:
rw [map_zero, add_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
@[simp]
lemma fst_compProd (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] :
    fst (κ ⊗ₖ η) = κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η).fst x) s = (κ x) s

Tactic:
simp [fst_compProd_apply, hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
⊢ (κ ⊗ₖ η).fst = κ

Tactic:
ext x s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η).fst x) s = (κ x) s
-- Mathlib/Data/Finsupp/Single.lean
theorem support_erase [DecidableEq α] {a : α} {f : α →₀ M} :
    (f.erase a).support = f.support.erase a

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = f.support.erase a

Tactic:
dsimp only [erase]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ f.support.erase a = f.support.erase a

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ f.support.erase a = f.support.erase a

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = f.support.erase a

Tactic:
classical
dsimp only [erase]
congr!

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem hom_ext {f g : FreeAlgebra R X →ₐ[R] A}
    (w : (f : FreeAlgebra R X → A) ∘ ι R = (g : FreeAlgebra R X → A) ∘ ι R) : f = g

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : (lift R).symm f = (lift R).symm g
⊢ f = g

Tactic:
exact (lift R).symm.injective w

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ⇑f ∘ ι R = ⇑g ∘ ι R
⊢ f = g

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : (lift R).symm f = (lift R).symm g
⊢ f = g
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.eq_of_openSegment_subset_frontier [Nontrivial 𝕜] [DenselyOrdered 𝕜]
    (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : openSegment 𝕜 x y ⊆ frontier s) :
    x = y

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y

Tactic:
by_contra hxy

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
hxy : ¬x = y
⊢ False

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
hxy : ¬x = y
⊢ False

Tactic:
exact
  (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
    (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y

Tactic:
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y

Tactic:
classical
  by_contra hxy
  exact
    (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
      (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.Plimit (o : Ordinal) (ho : Ordinal.IsLimit o) :
    (∀ (o' : Ordinal), o' < o → P I o') → P I o

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ (eval C)

Tactic:
rw [linearIndependent_iff_union_smaller C ho hsC, linearIndependent_subtype_iff]

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn ℤ id (⋃ e, smaller C ↑e)

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
⊢ (∀ o' < o, P I o') → P I o

Tactic:
intro h hho C hC hsC

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 => x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ (eval C)
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem constantCoeff_comp_map (f : R →+* S₁) :
    (constantCoeff : MvPolynomial σ S₁ →+* S₁).comp (MvPolynomial.map f) = f.comp constantCoeff :=
  by ext <;> simp

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ constantCoeff.comp (map f) = f.comp constantCoeff

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem Chain.eq_nil_of_irrefl [IsTrans α r] [IsIrrefl α r] (h : Chain r s) : s = Cycle.nil

Proof state:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h : Chain r s
⊢ s = Cycle.nil

Tactic:
induction' s with a l _ h

Result:
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h : Chain r Cycle.nil
⊢ Cycle.nil = Cycle.nil

case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
⊢ ↑(a :: l) = Cycle.nil

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
ha : a ∈ a :: l
⊢ ↑(a :: l) = Cycle.nil

Tactic:
exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Result:
no goals

Proof state:
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h : Chain r Cycle.nil
⊢ Cycle.nil = Cycle.nil

Tactic:
rfl

Result:
no goals

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
⊢ ↑(a :: l) = Cycle.nil

Tactic:
have ha := mem_cons_self a l

Result:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
ha : a ∈ a :: l
⊢ ↑(a :: l) = Cycle.nil
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_z : ¬ λ ∣ S.z := fun h ↦ by
  replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
  rw [coe_eta, ← z_spec, ← pow_two] at h
  exact lambda_sq_not_dvd_a_add_eta_sq_mul_b _ h

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.z S
⊢ False

Tactic:
replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.z S
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.z S
⊢ False

Tactic:
rw [coe_eta, ← z_spec, ← pow_two] at h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S.a + ↑η ^ 2 * S.b
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S.a + ↑η ^ 2 * S.b
⊢ False

Tactic:
exact lambda_sq_not_dvd_a_add_eta_sq_mul_b _ h

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_eq_rat_iff (hf : Continuous f) {m : ℤ} {n : ℕ} (hn : 0 < n) :
    τ f = m / n ↔ ∃ x, (f ^ n) x = x + m

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, (f ^ n) x = x + ↑m

Tactic:
exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)

Result:
no goals

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m

Tactic:
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]

Result:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, (f ^ n) x = x + ↑m