harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Function.lean
lemma SurjOn.prodMap (h₁ : SurjOn f₁ s₁ t₁) (h₂ : SurjOn f₂ s₂ t₂) :
    SurjOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Proof state:
case intro.intro.intro.intro
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Tactic:
exact ⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩

Result:
no goals

Proof state:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Tactic:
obtain ⟨a₁, ha₁, hx₁⟩ := h₁ hx.1

Result:
case intro.intro
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Proof state:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
⊢ SurjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
rintro x hx

Result:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Proof state:
case intro.intro
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Tactic:
obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2

Result:
case intro.intro.intro.intro
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_linearCombination (v) : b.repr (Finsupp.linearCombination _ b v) = v

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr ((linearCombination R ⇑b) v) = v

Tactic:
rw [← b.coe_repr_symm]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr (↑b.repr.symm v) = v

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr (↑b.repr.symm v) = v

Tactic:
exact b.repr.apply_symm_apply v

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Basic.lean
theorem comp_inv (φ : G →* H) (ψ : M →* G) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Proof state:
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
ext

Result:
case h
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
x✝ : M
⊢ (φ.comp ψ⁻¹) x✝ = (φ.comp ψ)⁻¹ x✝

Proof state:
case h
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
x✝ : M
⊢ (φ.comp ψ⁻¹) x✝ = (φ.comp ψ)⁻¹ x✝

Tactic:
simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
private
lemma cpow_mul_div_cpow_eq_div_div_cpow (m n : ℕ) (z : ℂ) (x : ℝ) :
    (n + 1) ^ (x : ℂ) * (z / m ^ (x : ℂ)) = z / (m / (n + 1)) ^ (x : ℂ)

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑m = ↑↑m

Tactic:
norm_cast

Result:
no goals

Proof state:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹

Tactic:
rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by simp,
  show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
  mul_cpow_ofReal_nonneg m.cast_nonneg Hn, mul_inv, mul_comm]

Result:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1)⁻¹ = ↑(↑n + 1)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

Tactic:
rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]

Result:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑n + 1 = ↑(↑n + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹

Tactic:
congr

Result:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹

Proof state:
m n : ℕ
z : ℂ
x : ℝ
⊢ 0 ≤ (↑n + 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Tactic:
rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
  Real.rpow_neg_one, inv_inv]

Result:
no goals

Proof state:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹

Tactic:
simp_rw [div_eq_mul_inv]

Result:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹

Proof state:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Tactic:
congr

Result:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Proof state:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ -↑x = ↑(-1) * ↑x

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
z : ℂ
x : ℝ
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

Tactic:
have Hn : (0 : ℝ) ≤ (n + 1 : ℝ)⁻¹ := by positivity

Result:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.add (hf : UniformConvexOn s φ f) (hg : UniformConvexOn s ψ g) :
    UniformConvexOn s (φ + ψ) (f + g)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖

Tactic:
simpa [mul_add, add_add_add_comm, sub_add_sub_comm]
  using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
⊢ UniformConvexOn s (φ + ψ) (f + g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_mem_star [InvolutiveStar α] : a⋆ ∈ s⋆ ↔ a ∈ s

Proof state:
α : Type u_1
s : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s

Tactic:
simp only [mem_star, star_star]

Result:
no goals
-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem separatedNhds_iff_disjoint {s t : Set X} : SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, exists_prop, ←
  exists_and_left, and_assoc, and_comm, and_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/HomologicalComplex.lean
lemma isSeparator_coproduct_separatingFamily {X : C} (hX : IsSeparator X) :
    IsSeparator (∐ (fun i ↦ separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
⊢ IsSeparator (∐ fun i => separatingFamily c (fun x => X) (PUnit.unit, i))

Tactic:
let φ (i : ι) := separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i => separatingFamily c (fun x => X) (PUnit.unit, i)
⊢ IsSeparator (∐ fun i => separatingFamily c (fun x => X) (PUnit.unit, i))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i => separatingFamily c (fun x => X) (PUnit.unit, i)
⊢ IsSeparating (Set.range fun x => X)

Tactic:
simpa using hX

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i => separatingFamily c (fun x => X) (PUnit.unit, i)
⊢ IsColimit
    (Cofan.mk (∐ φ) fun x =>
      match x with
      | (fst, i) => Sigma.ι φ i)

Tactic:
exact IsColimit.ofWhiskerEquivalence
  (Discrete.equivalence (Equiv.punitProd.{0} ι).symm) (coproductIsCoproduct φ)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i => separatingFamily c (fun x => X) (PUnit.unit, i)
⊢ IsSeparator (∐ fun i => separatingFamily c (fun x => X) (PUnit.unit, i))

Tactic:
refine isSeparator_of_isColimit_cofan
  (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using hX))
    (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type w
inst✝⁴ : DecidableEq ι
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i => separatingFamily c (fun x => X) (PUnit.unit, i)
⊢ IsColimit
    (Cofan.mk (∐ φ) fun x =>
      match x with
      | (fst, i) => Sigma.ι φ i)
-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma WEqualsLocallyBijective.transport (hG : CoverPreserving K J G) :
    J.WEqualsLocallyBijective A where
  iff f

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
  ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_nonpos_iff_forall_isMax : krullDim α ≤ 0 ↔ ∀ x : α, IsMax x

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0

Tactic:
rintro H ⟨_ | n, l, h⟩

Result:
case mk.zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), l i.castSucc < l i.succ
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0

case mk.succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), l i.castSucc < l i.succ
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0

Proof state:
α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ ![x, y] (Fin.castSucc 0) < ![x, y] (Fin.succ 0)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
i : Fin 1
⊢ ![x, y] i.castSucc < ![x, y] i.succ

Tactic:
obtain rfl := Subsingleton.elim i 0

Result:
α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ ![x, y] (Fin.castSucc 0) < ![x, y] (Fin.succ 0)

Proof state:
case mk.zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), l i.castSucc < l i.succ
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ 0 < ↑{ length := 1, toFun := ![x, y], step := ⋯ }.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ 0) ↔ ∀ (x b : α), ¬x < b

Tactic:
refine ⟨fun H x y h ↦ (H ⟨1, ![x, y],
  fun i ↦ by obtain rfl := Subsingleton.elim i 0; simpa⟩).not_lt (by simp), ?_⟩

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x

Tactic:
simp only [krullDim, iSup_le_iff, isMax_iff_forall_not_lt]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ 0) ↔ ∀ (x b : α), ¬x < b

Proof state:
case mk.succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), l i.castSucc < l i.succ
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0

Tactic:
cases H (l 0) (l 1) (h 0)

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem dvd_of_forall_prime_mul_dvd {a b : ℕ}
    (hdvd : ∀ p : ℕ, p.Prime → p ∣ a → p * a ∣ b) : a ∣ b

Proof state:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 1

Result:
case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b

case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b

Proof state:
case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b

Tactic:
apply one_dvd

Result:
no goals

Proof state:
case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b

Tactic:
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha

Result:
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b

Proof state:
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b

Tactic:
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem _root_.Set.PairwiseDisjoint.exists_mem_filter_basis {I : Type*} {l : I → Filter α}
    {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} {S : Set I}
    (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ i, (l i).HasBasis (p i) (s i)) :
    ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Proof state:
case intro.intro
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Tactic:
exact ⟨ind, hp, hd.mono ht⟩

Result:
no goals

Proof state:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Tactic:
rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩

Result:
case intro.intro
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Proof state:
case intro.intro
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Result:
case intro.intro
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem IsDecompOn.comp' {g f : X → X} {B A : Set X} {T S : Finset G}
    (hg : IsDecompOn g B T) (hf : IsDecompOn f A S) :
    IsDecompOn (g ∘ f) (A ∩ f ⁻¹' B) (T * S)

Proof state:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Tactic:
rcases hf _ aA with ⟨γ, γ_mem, hγ⟩

Result:
case intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Proof state:
case intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Tactic:
rcases hg _ aB with ⟨δ, δ_mem, hδ⟩

Result:
case intro.intro.intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Proof state:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
⊢ IsDecompOn (g ∘ f) (A ∩ f ⁻¹' B) (T * S)

Tactic:
intro _ ⟨aA, aB⟩

Result:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Proof state:
case intro.intro.intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Tactic:
use δ * γ, Finset.mul_mem_mul δ_mem γ_mem

Result:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ (g ∘ f) a✝ = (δ * γ) • a✝

Proof state:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ (g ∘ f) a✝ = (δ * γ) • a✝

Tactic:
rwa [mul_smul, ← hγ]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_max_aux₁ [CompleteSpace F] {f : ℂ → F} {z w : ℂ}
    (hd : DiffContOnCl ℂ f (ball z (dist w z)))
    (hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z) : ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
⊢ ‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖

Tactic:
rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this

Result:
no goals
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem prime_degree_dvd_card [CharZero F] (p_irr : Irreducible p) (p_deg : p.natDegree.Prime) :
    p.natDegree ∣ Fintype.card p.Gal

Proof state:
case a
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) ⋯ hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree

Tactic:
exact natDegree_le_of_dvd key (minpoly.ne_zero hα)

Result:
no goals