harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Path.lean
theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂)
    (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
δ₁ : Path a₂ a₃
γ₂ : Path b₁ b₂
δ₂ : Path b₂ b₃
⊢ (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Tactic:
ext t <;>
unfold Path.trans <;>
simp only [Path.coe_mk_mk, Path.prod_coe, Function.comp_apply] <;>
split_ifs <;>
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Function.Injective.sbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem RingFilterBasis.submodulesBasisIsBasis (BR : RingFilterBasis R) {B : ι → Submodule R M}
    (hB : BR.SubmodulesBasis B) : @_root_.SubmodulesBasis ι R _ M _ _ BR.topology B :=
  let _ := BR.topology
  { inter := hB.inter
    smul

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
intro m i

Result:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
letI := BR.topology

Result:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
rcases hB.smul m i with ⟨V, V_in, hV⟩

Result:
case intro.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableWithinAt_finCons :
    DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
      DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x

Tactic:
rw [differentiableWithinAt_pi, Fin.forall_fin_succ, differentiableWithinAt_pi]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) s x ∧
      ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) s x) ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x => φs x i) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) s x ∧
      ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) s x) ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x => φs x i) s x

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem injective_iff {α β} {f : Option α → β} :
    Injective f ↔ Injective (f ∘ some) ∧ f none ∉ range (f ∘ some)

Proof state:
case intro.none.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ none = none

case intro.none.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
b : α
hab : f none = f (some b)
⊢ none = some b

case intro.some.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a : α
hab : f (some a) = f none
⊢ some a = none

case intro.some.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a b : α
hab : f (some a) = f (some b)
⊢ some a = some b

Tactic:
exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f

Tactic:
rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab

Result:
case intro.none.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ none = none

case intro.none.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
b : α
hab : f none = f (some b)
⊢ none = some b

case intro.some.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a : α
hab : f (some a) = f none
⊢ some a = none

case intro.some.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a b : α
hab : f (some a) = f (some b)
⊢ some a = some b

Proof state:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none

Tactic:
refine
  ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩

Result:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.eq_of_closure_subset (hI : M.IsBasis I X) (hJI : J ⊆ I) (hJ : X ⊆ M.closure J) :
    J = I

Proof state:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ I ⊆ M.closure J

Tactic:
exact hI.subset.trans hJ

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ J = I

Tactic:
rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]

Result:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ I ⊆ M.closure J
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem mem_orbit_self (a : α) : a ∈ orbit M a :=
  ⟨1, by simp [MulAction.one_smul]⟩

Proof state:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (fun m => m • a) 1 = a

Tactic:
simp [MulAction.one_smul]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhdsLE_basis_of_exists_lt [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a

Proof state:
case h.e'_5.h.h
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ l, l < a
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ Ioc x✝ a = Ico a x✝

Tactic:
exact dual_Ico.symm

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ l, l < a
⊢ (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a

Tactic:
convert nhdsGE_basis_of_exists_gt (α := αᵒᵈ) ha using 2

Result:
case h.e'_5.h.h
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ l, l < a
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ Ioc x✝ a = Ico a x✝
-- Mathlib/Data/Nat/Size.lean
theorem size_pow {n : ℕ} : size (2 ^ n) = n + 1 :=
  le_antisymm (size_le.2 <| Nat.pow_lt_pow_right (by decide) (lt_succ_self _))
    (lt_size.2 <| le_rfl)

Proof state:
n : ℕ
⊢ 1 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Upto.lean
theorem wf : (∃ x, p x) → WellFounded (Upto.GT p)
  | ⟨x, h⟩ => by
    suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf
    ext ⟨a, ha⟩ ⟨b, _⟩
    dsimp [InvImage, Upto.GT]
    rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)]

Proof state:
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ j < a, ¬p j
b : ℕ
property✝ : ∀ j < b, ¬p j
⊢ Upto.GT p ⟨a, ha⟩ ⟨b, property✝⟩ ↔ InvImage (fun x1 x2 => x1 < x2) (fun y => x - ↑y) ⟨a, ha⟩ ⟨b, property✝⟩

Tactic:
dsimp [InvImage, Upto.GT]

Result:
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ j < a, ¬p j
b : ℕ
property✝ : ∀ j < b, ¬p j
⊢ a > b ↔ x - a < x - b

Proof state:
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ j < a, ¬p j
b : ℕ
property✝ : ∀ j < b, ¬p j
⊢ a > b ↔ x - a < x - b

Tactic:
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)]

Result:
no goals

Proof state:
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y

Tactic:
ext ⟨a, ha⟩ ⟨b, _⟩

Result:
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ j < a, ¬p j
b : ℕ
property✝ : ∀ j < b, ¬p j
⊢ Upto.GT p ⟨a, ha⟩ ⟨b, property✝⟩ ↔ InvImage (fun x1 x2 => x1 < x2) (fun y => x - ↑y) ⟨a, ha⟩ ⟨b, property✝⟩

Proof state:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y
⊢ WellFounded (InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y)

Tactic:
exact (measure _).wf

Result:
no goals

Proof state:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y
⊢ WellFounded (Upto.GT p)

Tactic:
rw [this]

Result:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y
⊢ WellFounded (InvImage (fun x1 x2 => x1 < x2) fun y => x - ↑y)
-- Mathlib/Probability/Kernel/Composition/ParallelComp.lean
lemma lintegral_parallelComp (κ : Kernel α β) [IsSFiniteKernel κ]
    (η : Kernel γ δ) [IsSFiniteKernel η]
    (ac : α × γ) {g : β × δ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ bd, g bd ∂(κ ∥ₖ η) ac = ∫⁻ b, ∫⁻ d, g (b, d) ∂η ac.2 ∂κ ac.1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), ∫⁻ (c : δ), g (b, c) ∂(prodMkLeft α η) ac ∂(prodMkRight γ κ) ac =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η) ac = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1

Tactic:
rw [parallelComp, lintegral_prod _ _ _ hg]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), ∫⁻ (c : δ), g (b, c) ∂(prodMkLeft α η) ac ∂(prodMkRight γ κ) ac =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem abs_mulExpNegMulSq_le (hε : 0 < ε) {x : ℝ} : |mulExpNegMulSq ε x| ≤ (sqrt ε)⁻¹

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹ * 1

Tactic:
rw [mul_le_mul_left (inv_pos.mpr (sqrt_pos_of_pos hε))]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

Tactic:
rw [mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x, abs_mul,
  abs_of_pos (inv_pos.mpr (sqrt_pos_of_pos hε))]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1

Tactic:
exact abs_mulExpNegMulSq_one_le_one (sqrt ε * x)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Tactic:
nth_rw 2 [← mul_one (sqrt ε)⁻¹]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹ * 1
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η * S.b)`. -/
lemma lambda_dvd_a_add_eta_mul_b : λ ∣ (S.a + η * S.b) :=
  a_add_eta_mul_b S ▸ dvd_add (dvd_trans (dvd_pow_self _ (by decide)) S.hab) ⟨S.b, by rw [mul_comm]⟩

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ λ * S.b = λ * S.b

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_id' (l : List (List α)) : l.flatMap (fun a => a) = l.flatten

Proof state:
α : Type u_1
l : List (List α)
⊢ flatMap (fun a => a) l = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_iSup_le {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal} (hf : BddAbove (range f))
    (w : ∀ i, lift.{u} (f i) ≤ t) : lift.{u} (iSup f) ≤ t

Proof state:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
rw [lift_iSup hf]

Result:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t

Proof state:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t

Tactic:
exact ciSup_le' w

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem continuous_left_toIocMod : ContinuousWithinAt (toIocMod hp a) (Iic x) x

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x y : 𝕜
⊢ toIocMod hp a y = toIocMod hp a (- -y)

Tactic:
rw [neg_neg]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x

Tactic:
have : ContinuousNeg 𝕜 := IsTopologicalAddGroup.toContinuousNeg

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
this : ContinuousNeg 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
this : ContinuousNeg 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x

Tactic:
exact
  (continuous_sub_left _).continuousAt.comp_continuousWithinAt <|
    (continuous_right_toIcoMod _ _ _).comp continuous_neg.continuousWithinAt fun y => neg_le_neg

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIocMod hp a) (Iic x) x

Tactic:
rw [(funext fun y => Eq.trans (by rw [neg_neg]) <| toIocMod_neg _ _ _ :
    toIocMod hp a = (fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg)]

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem inseparable_iff : Inseparable x y ↔ edist x y = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
⊢ Inseparable x y ↔ edist x y = 0

Tactic:
simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_lt_iff_le']

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem exists_strictMono' [NoMaxOrder α] (a : α) : ∃ f : ℕ → α, StrictMono f ∧ f 0 = a

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
choose g hg using fun x : α ↦ exists_gt x

Result:
α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a
-- Mathlib/LinearAlgebra/Dimension/Localization.lean
theorem exists_set_linearIndependent_of_isDomain [IsDomain R] :
    ∃ s : Set M, #s = Module.rank R M ∧ LinearIndepOn R id s

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ #↑(Set.range w) = Module.rank R M

Tactic:
apply Cardinal.lift_injective.{max u v}

Result:
case intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{max u v, v} #↑(Set.range w) = lift.{max u v, v} (Module.rank R M)

Proof state:
case intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{max u v, v} #↑(Set.range w) = lift.{max u v, v} (Module.rank R M)

Tactic:
rw [Cardinal.mk_range_eq_of_injective hw.injective, ← Module.Free.rank_eq_card_chooseBasisIndex,
IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl]

Result:
no goals

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ ∃ s, #↑s = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
refine ⟨Set.range w, ?_, (linearIndepOn_id_range_iff hw.injective).mpr hw⟩

Result:
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ #↑(Set.range w) = Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
⊢ ∃ s, #↑s = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
obtain ⟨w, hw⟩ :=
  IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl
    (Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M)).linearIndependent

Result:
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ ∃ s, #↑s = Module.rank R M ∧ LinearIndepOn R id s
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem card : Fintype.card (K →+* A) = finrank ℚ K

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ Fintype.card (K →+* A) = finrank ℚ K

Tactic:
rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem iSup_eq_closure {ι : Sort*} (p : ι → Subgroup G) :
    ⨆ i, p i = closure (⋃ i, (p i : Set G))

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem induce_mono (hg : G' ≤ G'') (hs : s ⊆ s') : G'.induce s ≤ G''.induce s'

Proof state:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
intro v w hv hw ha

Result:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Proof state:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Tactic:
simp +contextual only [induce_adj, and_imp]

Result:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Proof state:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
exact ⟨hs hv, hs hw, hg.2 ha⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ G'.induce s ≤ G''.induce s'

Tactic:
constructor

Result:
case left
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts

case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Proof state:
case left
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts

Tactic:
simp [hs]

Result:
no goals