harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Prod.lean
lemma compl_prod_eq_union {α β : Type*} (s : Set α) (t : Set β) :
    (s ×ˢ t)ᶜ = (sᶜ ×ˢ univ) ∪ (univ ×ˢ tᶜ)

Proof state:
case h.mpr
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∉ s ∨ p.2 ∉ t
⊢ p.1 ∈ s → p.2 ∉ t

Tactic:
intro fst_in_s

Result:
case h.mpr
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∉ s ∨ p.2 ∉ t
fst_in_s : p.1 ∈ s
⊢ p.2 ∉ t

Proof state:
α : Type u_5
β : Type u_6
s : Set α
t : Set β
⊢ (s ×ˢ t)ᶜ = sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

Tactic:
ext p

Result:
case h
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
⊢ p ∈ (s ×ˢ t)ᶜ ↔ p ∈ sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

Proof state:
case h
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
⊢ p.1 ∈ s → p.2 ∉ t ↔ p.1 ∉ s ∨ p.2 ∉ t

Tactic:
constructor <;> intro h

Result:
case h.mp
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
⊢ p.1 ∉ s ∨ p.2 ∉ t

case h.mpr
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∉ s ∨ p.2 ∉ t
⊢ p.1 ∈ s → p.2 ∉ t

Proof state:
case pos
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
fst_in_s : p.1 ∈ s
⊢ p.1 ∉ s ∨ p.2 ∉ t

Tactic:
exact Or.inr (h fst_in_s)

Result:
no goals

Proof state:
case h.mp
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
⊢ p.1 ∉ s ∨ p.2 ∉ t

Tactic:
by_cases fst_in_s : p.fst ∈ s

Result:
case pos
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
fst_in_s : p.1 ∈ s
⊢ p.1 ∉ s ∨ p.2 ∉ t

case neg
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
fst_in_s : p.1 ∉ s
⊢ p.1 ∉ s ∨ p.2 ∉ t

Proof state:
case h.mpr
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∉ s ∨ p.2 ∉ t
fst_in_s : p.1 ∈ s
⊢ p.2 ∉ t

Tactic:
simpa only [fst_in_s, not_true, false_or] using h

Result:
no goals

Proof state:
case neg
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
h : p.1 ∈ s → p.2 ∉ t
fst_in_s : p.1 ∉ s
⊢ p.1 ∉ s ∨ p.2 ∉ t

Tactic:
exact Or.inl fst_in_s

Result:
no goals

Proof state:
case h
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
⊢ p ∈ (s ×ˢ t)ᶜ ↔ p ∈ sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

Tactic:
simp only [mem_compl_iff, mem_prod, not_and, mem_union, mem_univ, and_true, true_and]

Result:
case h
α : Type u_5
β : Type u_6
s : Set α
t : Set β
p : α × β
⊢ p.1 ∈ s → p.2 ∉ t ↔ p.1 ∉ s ∨ p.2 ∉ t
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem pNilradical_eq_bot {R : Type*} [CommSemiring R] {p : ℕ} (hp : ¬ 1 < p) :
    pNilradical R p = ⊥

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ pNilradical R p = ⊥

Tactic:
rw [pNilradical, if_neg hp]

Result:
no goals
-- Mathlib/Algebra/AlgebraicCard.lean
theorem countable : Set.Countable { x : A | IsAlgebraic R x }

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ {x | IsAlgebraic R x}.Countable

Tactic:
rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]

Result:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift.{?u.19622, v} #↑{x | IsAlgebraic R x} ≤ ℵ₀

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift.{?u.19622, v} #↑{x | IsAlgebraic R x} ≤ ℵ₀

Tactic:
apply (cardinalMk_lift_le_max R A).trans

Result:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift.{v, u} #R ⊔ ℵ₀ ≤ ℵ₀

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : Countable R
⊢ lift.{v, u} #R ⊔ ℵ₀ ≤ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem forall_eq_iff_forall_eq : (∀ f g : R[X], f = g) ↔ ∀ a b : R, a = b

Proof state:
R : Type u
inst✝ : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem reaches₁_eq {σ} {f : σ → Option σ} {a b c} (h : f a = f b) :
    Reaches₁ f a c ↔ Reaches₁ f b c :=
  TransGen.head'_iff.trans (TransGen.head'_iff.trans <| by rw [h]).symm

Proof state:
σ : Type u_1
f : σ → Option σ
a b c : σ
h : f a = f b
⊢ (∃ b_1 ∈ f b, ReflTransGen (fun a b => b ∈ f a) b_1 c) ↔ ∃ b ∈ f a, ReflTransGen (fun a b => b ∈ f a) b c

Tactic:
rw [h]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_f_0_comp_zeroCochainsLequiv :
    (cochainsMap f φ).f 0 ≫ (zeroCochainsLequiv B).toModuleIso.hom =
      (zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom

Proof state:
case hf.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 0)
⊢ (ModuleCat.Hom.hom
        ((ModuleCat.ofHom (LinearMap.funLeft k ↑A.V fun x => default) ≫
            ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (Fin 0 → G))) ≫
          (zeroCochainsLequiv B).toModuleIso.hom))
      x =
    (ModuleCat.Hom.hom ((zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom)) x

Tactic:
rfl

Result:
no goals

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cochainsMap f φ).f 0 ≫ (zeroCochainsLequiv B).toModuleIso.hom = (zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom

Tactic:
ext x

Result:
case hf.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 0)
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (zeroCochainsLequiv B).toModuleIso.hom)) x =
    (ModuleCat.Hom.hom ((zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom)) x

Proof state:
case hf.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 0)
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (zeroCochainsLequiv B).toModuleIso.hom)) x =
    (ModuleCat.Hom.hom ((zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom)) x

Tactic:
simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]

Result:
case hf.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 0)
⊢ (ModuleCat.Hom.hom
        ((ModuleCat.ofHom (LinearMap.funLeft k ↑A.V fun x => default) ≫
            ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (Fin 0 → G))) ≫
          (zeroCochainsLequiv B).toModuleIso.hom))
      x =
    (ModuleCat.Hom.hom ((zeroCochainsLequiv A).toModuleIso.hom ≫ φ.hom)) x
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem fixedBy_subset_fixedBy_zpow (g : G) (j : ℤ) :
    fixedBy α g ⊆ fixedBy α (g ^ j)

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
j : ℤ
a : α
a_in_fixedBy : a ∈ fixedBy α g
⊢ 1 ∣ j

Tactic:
exact one_dvd j

Result:
no goals

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
j : ℤ
⊢ fixedBy α g ⊆ fixedBy α (g ^ j)

Tactic:
intro a a_in_fixedBy

Result:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
j : ℤ
a : α
a_in_fixedBy : a ∈ fixedBy α g
⊢ a ∈ fixedBy α (g ^ j)

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
j : ℤ
a : α
a_in_fixedBy : a ∈ fixedBy α g
⊢ a ∈ fixedBy α (g ^ j)

Tactic:
rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd,
  minimalPeriod_eq_one_iff_fixedBy.mpr a_in_fixedBy, Int.natCast_one]

Result:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
j : ℤ
a : α
a_in_fixedBy : a ∈ fixedBy α g
⊢ 1 ∣ j
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mem_rat_span_latticeBasis [NumberField K] (x : K) :
    canonicalEmbedding K x ∈ Submodule.span ℚ (Set.range (latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      ((integralBasis K).repr x) x_1 • (canonicalEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
refine Submodule.sum_smul_mem _ _ (fun i _ ↦ Submodule.subset_span ?_)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (canonicalEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      (canonicalEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
simp_rw [map_rat_smul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      ((integralBasis K).repr x) x_1 • (canonicalEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
rw [← Basis.sum_repr (integralBasis K) x, map_sum]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K),
      (canonicalEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)

Tactic:
exact Set.mem_range_self i

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (canonicalEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Tactic:
rw [← latticeBasis_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sq : sinh x ^ 2 = cosh x ^ 2 - 1

Proof state:
x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
rw [← cosh_sq_sub_sinh_sq x]

Result:
x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - (cosh x ^ 2 - sinh x ^ 2)

Proof state:
x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - (cosh x ^ 2 - sinh x ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Icc : (Icc a b).map Fin.valEmbedding = Icc ↑a ↑b

Proof state:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Icc a b) = Icc ↑a ↑b

Tactic:
simp [Icc_eq_finset_subtype, Finset.fin, Finset.map_map, Icc_filter_lt_of_lt_right]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Matroidᵣ.coe_inj {M₁ M₂ : Matroidᵣ α} :
    (M₁ : Matroid α) = (M₂ : Matroid α) ↔ M₁ = M₂

Proof state:
α : Type u_1
M₁ M₂ : Matroidᵣ α
⊢ M₁.toMatroid = M₂.toMatroid ↔ M₁ = M₂

Tactic:
cases M₁

Result:
case ofMatroid
α : Type u_1
M₂ : Matroidᵣ α
toMatroid✝ : Matroid α
⊢ { toMatroid := toMatroid✝ }.toMatroid = M₂.toMatroid ↔ { toMatroid := toMatroid✝ } = M₂

Proof state:
case ofMatroid.ofMatroid
α : Type u_1
toMatroid✝¹ toMatroid✝ : Matroid α
⊢ { toMatroid := toMatroid✝¹ }.toMatroid = { toMatroid := toMatroid✝ }.toMatroid ↔
    { toMatroid := toMatroid✝¹ } = { toMatroid := toMatroid✝ }

Tactic:
simp

Result:
no goals

Proof state:
case ofMatroid
α : Type u_1
M₂ : Matroidᵣ α
toMatroid✝ : Matroid α
⊢ { toMatroid := toMatroid✝ }.toMatroid = M₂.toMatroid ↔ { toMatroid := toMatroid✝ } = M₂

Tactic:
cases M₂

Result:
case ofMatroid.ofMatroid
α : Type u_1
toMatroid✝¹ toMatroid✝ : Matroid α
⊢ { toMatroid := toMatroid✝¹ }.toMatroid = { toMatroid := toMatroid✝ }.toMatroid ↔
    { toMatroid := toMatroid✝¹ } = { toMatroid := toMatroid✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq' {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x)

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ decide (∀ (x : α), x ∈ xs → p x = true) = decide (∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true)

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = decide (∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true)

Tactic:
simp only [all_mk, Array.all_eq']

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ decide (∀ (x : α), x ∈ xs → p x = true) = decide (∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true)

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = decide (∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true)
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycle_iff_exists_isCycleOn :
    f.IsCycle ↔ ∃ s : Set α, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x⦄, ¬IsFixedPt f x → x ∈ s

Proof state:
case refine_1.intro
α : Type u_2
f : Perm α
a : α
ha : f a ≠ a ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle a y
⊢ {x | f x ≠ x}.Nontrivial

Tactic:
exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
⊢ f.IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle

Proof state:
case refine_1
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ {x | f x ≠ x}.Nontrivial

Tactic:
obtain ⟨a, ha⟩ := hf

Result:
case refine_1.intro
α : Type u_2
f : Perm α
a : α
ha : f a ≠ a ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle a y
⊢ {x | f x ≠ x}.Nontrivial

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle

Tactic:
exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_2
f : Perm α
⊢ (∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s) → f.IsCycle

Tactic:
rintro ⟨s, hs, hf, hsf⟩

Result:
case refine_2.intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
⊢ f.IsCycle

Proof state:
α : Type u_2
f : Perm α
⊢ f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s

Tactic:
refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩

Result:
case refine_1
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ {x | f x ≠ x}.Nontrivial

case refine_2
α : Type u_2
f : Perm α
⊢ (∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s) → f.IsCycle
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashSeq_eq_self_of_terminated (terminatedAt_succ_n : s.TerminatedAt (n + 1)) :
    squashSeq s n = s

Proof state:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
⊢ squashSeq s n = s

Tactic:
cases s_nth_eq : s.get? n <;> simp only [*, squashSeq]

Result:
no goals

Proof state:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.TerminatedAt (n + 1)
⊢ squashSeq s n = s

Tactic:
change s.get? (n + 1) = none at terminatedAt_succ_n

Result:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
⊢ squashSeq s n = s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_extract (a : Vector α n) (start stop) :
    (a.extract start stop).toList = (a.toList.drop start).take (stop - start)

Proof state:
α : Type u_1
n : Nat
a : Vector α n
start stop : Nat
⊢ (a.extract start stop).toList = List.take (stop - start) (List.drop start a.toList)

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/ComputeDegree.lean
theorem coeff_add_of_eq {n : ℕ} {a b : R} {f g : R[X]}
    (h_add_left : f.coeff n = a) (h_add_right : g.coeff n = b) :
    (f + g).coeff n = a + b

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
⊢ (f + g).coeff n = a + b

Tactic:
subst ‹_› ‹_›

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n

Tactic:
apply coeff_add

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l

Tactic:
intro
| Or.inl h' => rw [h']; exact h
| Or.inr h' => exact h'

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ a ∈ l

Tactic:
rw [h']

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ b ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : ¬b ∈ l
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l

Tactic:
rw [insert_of_not_mem h, mem_cons]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ l ↔ a = b ∨ a ∈ l

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ l → a = b ∨ a ∈ l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l

Tactic:
if h : b ∈ l then
  rw [insert_of_mem h]
  constructor; {apply Or.inr}
  intro
  | Or.inl h' => rw [h']; exact h
  | Or.inr h' => exact h'
else rw [insert_of_not_mem h, mem_cons]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ l → a = b ∨ a ∈ l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l

Tactic:
{apply Or.inr}

Result:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a = b ∨ a ∈ l → a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a ∈ l
⊢ a ∈ l

Tactic:
exact h'

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ l → a = b ∨ a ∈ l

Tactic:
apply Or.inr

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
x✝ : a = b ∨ a ∈ l
h' : a = b
⊢ b ∈ l

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ List.insert b l ↔ a = b ∨ a ∈ l

Tactic:
rw [insert_of_mem h]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
l : List α
h : b ∈ l
⊢ a ∈ l ↔ a = b ∨ a ∈ l
-- Mathlib/Analysis/Convex/Segment.lean
theorem midpoint_mem_segment [Invertible (2 : 𝕜)] (x y : E) : midpoint 𝕜 x y ∈ [x -[𝕜] y]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ [x-[𝕜]y]

Tactic:
rw [segment_eq_image_lineMap]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ⇑(AffineMap.lineMap x y) '' Icc 0 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ⇑(AffineMap.lineMap x y) '' Icc 0 1

Tactic:
exact ⟨⅟ 2, ⟨invOf_nonneg.mpr zero_le_two, invOf_le_one one_le_two⟩, rfl⟩

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma δ_one_mkOfSucc {n : ℕ} (i : Fin n) :
    δ 1 ≫ mkOfSucc i = SimplexCategory.const _ _ i.castSucc

Proof state:
case a.h.h.h
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ ↑↑i.castSucc)) x)

Tactic:
fin_cases x

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ ↑↑i.castSucc)) ((fun i => i) ⟨0, ⋯⟩))

Proof state:
n : ℕ
i : Fin n
⊢ δ 1 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ ↑↑i.castSucc

Tactic:
ext x

Result:
case a.h.h.h
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ ↑↑i.castSucc)) x)

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ ↑↑i.castSucc)) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem union_comm_of_disjoint {s₁ s₂ : Finmap β} : Disjoint s₁ s₂ → s₁ ∪ s₂ = s₂ ∪ s₁ :=
  induction_on₂ s₁ s₂ fun s₁ s₂ => by
    intro h
    simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ⟦s₁⟧.Disjoint ⟦s₂⟧
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧

Tactic:
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ⟦s₁⟧.Disjoint ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧

Tactic:
intro h

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ⟦s₁⟧.Disjoint ⟦s₂⟧
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem range_exp : Set.range exp = {0}ᶜ :=
  Set.ext fun x =>
    ⟨by
      rintro ⟨x, rfl⟩
      exact exp_ne_zero x, fun hx => ⟨log x, exp_log hx⟩⟩

Proof state:
x : ℂ
⊢ x ∈ Set.range cexp → x ∈ {0}ᶜ

Tactic:
rintro ⟨x, rfl⟩

Result:
case intro
x : ℂ
⊢ cexp x ∈ {0}ᶜ

Proof state:
case intro
x : ℂ
⊢ cexp x ∈ {0}ᶜ

Tactic:
exact exp_ne_zero x

Result:
no goals