harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem Int.not_isField : ¬IsField ℤ := fun h =>
  Int.not_even_one <|
    (h.mul_inv_cancel two_ne_zero).imp fun a => by rw [← two_mul]; exact Eq.symm

Proof state:
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = a + a

Tactic:
rw [← two_mul]

Result:
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = 2 * a

Proof state:
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = 2 * a

Tactic:
exact Eq.symm

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem Obj.map_epi_on_summand_id {Δ Δ' : SimplexCategory} (e : Δ' ⟶ Δ) [Epi e] :
    ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op Δ)) ≫ (Γ₀.obj K).map e.op =
      ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.mk e)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
inst✝¹ : HasFiniteCoproducts C
Δ Δ' : SimplexCategory
e : Δ' ⟶ Δ
inst✝ : Epi e
⊢ ((splitting K).cofan (op Δ)).inj (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op =
    ((splitting K).cofan (op Δ')).inj (Splitting.IndexSet.mk e)

Tactic:
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op
    (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
  Γ₀.Obj.Termwise.mapMono_id] using id_comp _

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
protected lemma Derives.reverse (hg : g.Derives u v) : g.reverse.Derives u.reverse v.reverse

Proof state:
case tail
T : Type u_1
g : ContextFreeGrammar T
u v b✝ c✝ : List (Symbol T g.NT)
a✝ : Relation.ReflTransGen g.Produces u b✝
orig : g.Produces b✝ c✝
ih : g.reverse.Derives u.reverse b✝.reverse
⊢ g.reverse.Derives u.reverse c✝.reverse

Tactic:
exact ih.trans_produces orig.reverse

Result:
no goals

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hg : g.Derives u v
⊢ g.reverse.Derives u.reverse v.reverse

Tactic:
induction hg with
| refl => rfl
| tail _ orig ih => exact ih.trans_produces orig.reverse

Result:
no goals

Proof state:
case refl
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u.reverse u.reverse

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_pow (f : R) (n : ℕ) (hn : 0 < n) : basicOpen (f ^ n) = basicOpen f :=
  TopologicalSpace.Opens.ext <| by simpa using zeroLocus_singleton_pow f n hn

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen (f ^ n)) = ↑(basicOpen f)

Tactic:
simpa using zeroLocus_singleton_pow f n hn

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_two_mul : sinh (2 * x) = 2 * sinh x * cosh x

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

Tactic:
rw [two_mul, sinh_add]

Result:
x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x

Proof state:
x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x

Tactic:
ring

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_id :
    map I (LinearMap.id (M := M)) =
      LinearMap.id (R := AdicCompletion I R) (M := AdicCompletion I M)

Proof state:
case h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : AdicCauchySequence I M
n : ℕ
⊢ ↑((map I LinearMap.id) ((mk I M) a)) n = ↑(LinearMap.id ((mk I M) a)) n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ map I LinearMap.id = LinearMap.id

Tactic:
ext a n

Result:
case h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : AdicCauchySequence I M
n : ℕ
⊢ ↑((map I LinearMap.id) ((mk I M) a)) n = ↑(LinearMap.id ((mk I M) a)) n
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_lf {a b : Ordinal} (h : a < b) : a.toPGame ⧏ b.toPGame

Proof state:
a b : Ordinal.{u_1}
h : a < b
⊢ a.toPGame ⧏ b.toPGame

Tactic:
convert moveLeft_lf (toLeftMovesToPGame ⟨a, h⟩)

Result:
case h.e'_1
a b : Ordinal.{u_1}
h : a < b
⊢ a.toPGame = b.toPGame.moveLeft (toLeftMovesToPGame ⟨a, h⟩)

Proof state:
case h.e'_1
a b : Ordinal.{u_1}
h : a < b
⊢ a.toPGame = b.toPGame.moveLeft (toLeftMovesToPGame ⟨a, h⟩)

Tactic:
rw [toPGame_moveLeft]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h} :
    m.getKey a h = m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.WF
a fallback : α
h : a ∈ m
⊢ m.getKey a h = m.getKeyD a fallback

Tactic:
simp_to_raw using Raw₀.getKey_eq_getKeyD

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_left [DecidableEq α] (h : t.Nonempty) : image₂ (fun x _ => x) s t = s :=
  coe_injective <| by
    push_cast
    exact image2_left h

Proof state:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq α
h : t.Nonempty
⊢ image2 (fun x x_1 => x) ↑s ↑t = ↑s

Tactic:
exact image2_left h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq α
h : t.Nonempty
⊢ ↑(image₂ (fun x x_1 => x) s t) = ↑s

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq α
h : t.Nonempty
⊢ image2 (fun x x_1 => x) ↑s ↑t = ↑s
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.tendsto_div_nhds_zero {f g : α → 𝕜} (h : f =o[l] g) :
    Tendsto (fun x => f x / g x) l (𝓝 0) :=
  (isLittleO_one_iff 𝕜).mp <| by
    calc
      (fun x => f x / g x) =o[l] fun x => g x / g x

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
⊢ (fun x => f x / g x) =o[l] fun _x => 1

Tactic:
calc
  (fun x => f x / g x) =o[l] fun x => g x / g x := by
    simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)
  _ =O[l] fun _x => (1 : 𝕜) := isBigO_of_le _ fun x => by simp [div_self_le_one]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
⊢ (fun x => f x / g x) =o[l] fun x => g x / g x

Tactic:
simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
x : α
⊢ ‖g x / g x‖ ≤ ‖1‖

Tactic:
simp [div_self_le_one]

Result:
no goals
-- Mathlib/Data/Finset/Finsupp.lean
theorem card_finsupp (s : Finset ι) (t : ι → Finset α) : #(s.finsupp t) = ∏ i ∈ s, #(t i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
⊢ #(s.finsupp t) = ∏ i ∈ s, #(t i)

Tactic:
classical exact (card_map _).trans <| card_pi _ _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
⊢ #(s.finsupp t) = ∏ i ∈ s, #(t i)

Tactic:
exact (card_map _).trans <| card_pi _ _

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ Ordering.gt :=
  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> decide

Proof state:
m n : PosNum
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n <;> decide

Result:
no goals

Proof state:
m n : PosNum
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]

Result:
m n : PosNum
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬y ≤ x → ∀ᶠ z in l, ¬y ≤ f z

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : α), ¬y ≤ x → ∀ᶠ (z : β) in l, ¬y ≤ f z

Tactic:
simp [topology_eq_lowerTopology, tendsto_nhds_generateFrom_iff, Filter.Eventually, Ici,
  compl_setOf]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma erase_sup_Iic (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : s.erase a ⊔ Iic a = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, a ≤ b → b = a
⊢ s.erase a ⊔ Iic a = s

Tactic:
rw [← lowerClosure_singleton, ← sdiff_singleton, sdiff_sup_lowerClosure] <;> simpa

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleIntegrable_zero_radius {f : ℂ → E} {c : ℂ} : CircleIntegrable f c 0

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
⊢ CircleIntegrable f c 0

Tactic:
simp [CircleIntegrable]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Prod.lean
theorem isLinearMap_sub [AddCommGroup M] [Module R M] :
    IsLinearMap R fun x : M × M => x.1 - x.2

Proof state:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).1 - (x • y).2 = x • (y.1 - y.2)

Tactic:
simp [smul_sub]

Result:
no goals

Proof state:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M × M
⊢ (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)

Tactic:
simp [add_comm, add_assoc, add_left_comm, sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsLinearMap R fun x => x.1 - x.2

Tactic:
apply IsLinearMap.mk

Result:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)

case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)

Proof state:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)

Tactic:
intro x y

Result:
case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).1 - (x • y).2 = x • (y.1 - y.2)

Proof state:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)

Tactic:
intro x y

Result:
case map_add
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M × M
⊢ (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma continuousOn_tangentCoordChange (x y : M) : ContinuousOn (tangentCoordChange I x y)
    ((extChartAt I x).source ∩ (extChartAt I y).source)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
⊢ ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)

Tactic:
convert (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y) <;>
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
    (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b

Proof state:
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
exact if a0 : a = 0 then
  a0.symm ▸ H0 b
else
  have _ := mod_lt b a0
  H1 _ _ a0 (GCD.induction (b % a) a H0 H1)

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
classical
exact if a0 : a = 0 then
  a0.symm ▸ H0 b
else
  have _ := mod_lt b a0
  H1 _ _ a0 (GCD.induction (b % a) a H0 H1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ (do
      let a ← x
      pure (id a)) =
    x

Tactic:
rw [bind_pure_comp, id_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ x >>= pure = x

Tactic:
show x >>= (fun a => pure (id a)) = x

Result:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ (do
      let a ← x
      pure (id a)) =
    x
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_conj : SameCycle (g * f * g⁻¹) x y ↔ SameCycle f (g⁻¹ x) (g⁻¹ y) :=
  exists_congr fun i => by simp [conj_zpow, eq_inv_iff_eq]

Proof state:
α : Type u_2
f g : Perm α
x y : α
i : ℤ
⊢ ((g * f * g⁻¹) ^ i) x = y ↔ (f ^ i) (g⁻¹ x) = g⁻¹ y

Tactic:
simp [conj_zpow, eq_inv_iff_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma IsBase.mapEmbedding {B : Set α} (hB : M.IsBase B) (f : α ↪ β) :
    (M.mapEmbedding f).IsBase (f '' B)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ (M.mapEmbedding f).IsBase (⇑f '' B)

Tactic:
rw [Matroid.mapEmbedding, map_isBase_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ ∃ B₀, M.IsBase B₀ ∧ ⇑f '' B = ⇑f '' B₀

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ ∃ B₀, M.IsBase B₀ ∧ ⇑f '' B = ⇑f '' B₀

Tactic:
exact ⟨B, hB, rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
@[simp]
lemma toFinite_eq_zero_iff [SFinite μ] : μ.toFinite = 0 ↔ μ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ.toFinite = 0 ↔ μ = 0

Tactic:
simp_rw [← Measure.measure_univ_eq_zero, toFinite_apply_eq_zero_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
lemma hasZeroObject_of_additive [HasZeroObject C] :
    HasZeroObject D where
  zero := ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : HasZeroObject C
⊢ IsZero (F.obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[]

Proof state:
α✝ : Type u_1
l : Array α✝
h : 0 < l.size
⊢ l ≠ #[]

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
toList✝ : List α✝
h : 0 < { toList := toList✝ }.size
⊢ { toList := toList✝ } ≠ #[]

Proof state:
case mk
α✝ : Type u_1
toList✝ : List α✝
h : 0 < { toList := toList✝ }.size
⊢ { toList := toList✝ } ≠ #[]

Tactic:
simpa using List.ne_nil_of_length_pos h

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive]
lemma not_mulDissociated_iff_exists_disjoint :
    ¬ MulDissociated s ↔
      ∃ t u : Finset α, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Tactic:
refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
  Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast <;> exact diff_subset.trans ‹_›

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Tactic:
classical
refine not_mulDissociated.trans
  ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
rintro ⟨t, ht, u, hu, htu, h⟩
refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
  Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast <;> exact diff_subset.trans ‹_›

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Tactic:
refine not_mulDissociated.trans
  ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩

Result:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ (∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x) →
    ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Proof state:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ (∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x) →
    ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a

Tactic:
rintro ⟨t, ht, u, hu, htu, h⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
-- Mathlib/Order/Bounds/Basic.lean
theorem IsLeast.insert [LinearOrder γ] (a) {b} {s : Set γ} (hs : IsLeast s b) :
    IsLeast (insert a s) (min a b)

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast ({a} ∪ s) (a ⊓ b)

Tactic:
exact isLeast_singleton.union hs

Result:
no goals

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast (insert a s) (a ⊓ b)

Tactic:
rw [insert_eq]

Result:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast ({a} ∪ s) (a ⊓ b)
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem modByMonicHom_root_pow (h : IsAdjoinRootMonic S f) {n : ℕ} (hdeg : n < natDegree f) :
    h.modByMonicHom (h.root ^ n) = X ^ n

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ ↑n < f.degree

Tactic:
contrapose! hdeg

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
a✝ : Nontrivial R
hdeg : f.degree ≤ ↑n
⊢ f.natDegree ≤ n

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.root ^ n) = X ^ n

Tactic:
rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.Monic, degree_X_pow]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ ↑n < f.degree

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
a✝ : Nontrivial R
hdeg : f.degree ≤ ↑n
⊢ f.natDegree ≤ n

Tactic:
simpa [natDegree_le_iff_degree_le] using hdeg

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
⊢ h.modByMonicHom (h.root ^ n) = X ^ n

Tactic:
nontriviality R

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.root ^ n) = X ^ n
-- Mathlib/Data/Vector3.lean
theorem insert_fz (a : α) (v : Vector3 α n) : insert a v fz = a :: v

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
refine funext fun j => j.cases' ?_ ?_ <;> intros <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_sInter_subset (S : Set (Set α)) (f : α → β) : f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Proof state:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
rw [sInter_eq_biInter]

Result:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s

Proof state:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s

Tactic:
apply image_iInter₂_subset

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem gc_set :
    @GaloisConnection (Set A) (Set (ProjectiveSpectrum 𝒜))ᵒᵈ _ _
      (fun s => zeroLocus 𝒜 s) fun t => vanishingIdeal t

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)

Tactic:
simpa [zeroLocus_span, Function.comp_def] using GaloisConnection.compose ideal_gc (gc_ideal 𝒜)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)

Tactic:
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).1.isEmpty = (((m.1.isEmpty || (m.1.size == 1 && m.contains k))) &&
      (f (m.get? k)).isNone)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).val.isEmpty = ((m.val.isEmpty || m.val.size == 1 && m.contains k) && (f (m.get? k)).isNone)

Tactic:
simp_to_model [alter] using List.isEmpty_alterKey

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma fst_opProdIsoCoprod_hom : prod.fst.op ≫ (opProdIsoCoprod A B).hom = coprod.inl

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.fst.op ≫ (opProdIsoCoprod A B).hom = coprod.inl

Tactic:
rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, Quiver.Hom.op_unop]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem tail {n f} (hf : @Partrec' n f) : @Partrec' n.succ fun v => f v.tail :=
  (hf.comp _ fun i => @prim _ _ <| Nat.Primrec'.get i.succ).of_eq fun v => by
    simp; rw [← ofFn_get v.tail]; congr; funext i; simp

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)

Tactic:
congr

Result:
case e_a.e_a
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (fun i => v.get i.succ) = v.tail.get

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f v.tail

Tactic:
rw [← ofFn_get v.tail]

Result:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)

Proof state:
case e_a.e_a
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (fun i => v.get i.succ) = v.tail.get

Tactic:
funext i

Result:
case e_a.e_a.h
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
i : Fin n
⊢ v.get i.succ = v.tail.get i

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (mOfFn fun i => (↑fun v => v.get i.succ) v) >>= f = f v.tail

Tactic:
simp

Result:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i => v.get i.succ) = f v.tail

Proof state:
case e_a.e_a.h
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
i : Fin n
⊢ v.get i.succ = v.tail.get i

Tactic:
simp

Result:
no goals