harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Preimage.lean
theorem sigma_preimage_mk {β : α → Type*} [DecidableEq α] (s : Finset (Σa, β a)) (t : Finset α) :
    (t.sigma fun a => s.preimage (Sigma.mk a) sigma_mk_injective.injOn) =
      s.filter fun a => a.1 ∈ t

Proof state:
case h
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ t.sigma fun a => s.preimage (Sigma.mk a) ⋯) ↔ x ∈ filter (fun a => a.fst ∈ t) s

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
⊢ (t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = filter (fun a => a.fst ∈ t) s

Tactic:
ext x

Result:
case h
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ t.sigma fun a => s.preimage (Sigma.mk a) ⋯) ↔ x ∈ filter (fun a => a.fst ∈ t) s
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem mem_integerSet {a : mixedSpace K} :
    a ∈ integerSet K ↔ a ∈ fundamentalCone K ∧ ∃ x : 𝓞 K, mixedEmbedding K x = a

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : mixedSpace K
⊢ a ∈ integerSet K ↔ a ∈ fundamentalCone K ∧ ∃ x, (mixedEmbedding K) ↑x = a

Tactic:
simp only [integerSet, Set.mem_inter_iff, SetLike.mem_coe, LinearMap.mem_range,
  AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, RingHom.coe_comp, Function.comp_apply]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathComponentIn_univ (x : X) : pathComponentIn x univ = pathComponent x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ pathComponentIn x univ = pathComponent x

Tactic:
simp [pathComponentIn, pathComponent, JoinedIn, Joined, exists_true_iff_nonempty]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
lemma disjoint_edgeFinset : Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂

Tactic:
simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem intCast_coeff_zero {i : ℤ} {R : Type*} [Ring R] : (i : R[X]).coeff 0 = i

Proof state:
i : ℤ
R : Type u_1
inst✝ : Ring R
⊢ (↑i).coeff 0 = ↑i

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem reduce_v : ∀ u : XgcdType, u.reduce.v = u.v
  | u =>
    dite (u.r = 0) (fun h => by rw [reduce_a h, finish_v u h]) fun h => by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.v = x✝.v

Tactic:
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]

Result:
no goals

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ x✝.reduce.v = x✝.v

Tactic:
rw [reduce_a h, finish_v u h]

Result:
no goals

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
⊢ x✝.reduce.v = x✝.v

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.v = x✝.v
-- Mathlib/Algebra/CharP/Two.lean
theorem neg_one_eq_one_iff [Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ -1 = 1 ↔ ringChar R = 2

Tactic:
refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ↑(1 + 1) = 0
⊢ ringChar R = 2

Tactic:
exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2

Tactic:
rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ↑(1 + 1) = 0
⊢ ringChar R = 2
-- Mathlib/Order/Partition/Finpartition.lean
theorem parts_top_subset (a : α) [Decidable (a = ⊥)] : (⊤ : Finpartition a).parts ⊆ {a}

Proof state:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ ((Finpartition.empty α).copy ⋯).parts
⊢ b ∈ {a}

Tactic:
simp only [copy_parts, empty_parts, not_mem_empty] at hb

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
⊢ ⊤.parts ⊆ {a}

Tactic:
intro b hb

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha).parts
⊢ b ∈ {a}

Tactic:
split_ifs at hb

Result:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ ((Finpartition.empty α).copy ⋯).parts
⊢ b ∈ {a}

case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}

Proof state:
case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}

Tactic:
exact hb

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}

Tactic:
have hb : b ∈ Finpartition.parts (dite _ _ _) := hb

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha).parts
⊢ b ∈ {a}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c

Proof state:
case succ
b c a : Nat
ih : 0 < a → (a * b < a * c ↔ b < c)
a0 : 0 < a + 1
⊢ (a + 1) * b < (a + 1) * c ↔ b < c

Tactic:
cases a

Result:
case succ.zero
b c : Nat
ih : 0 < 0 → (0 * b < 0 * c ↔ b < c)
a0 : 0 < 0 + 1
⊢ (0 + 1) * b < (0 + 1) * c ↔ b < c

case succ.succ
b c n✝ : Nat
ih : 0 < n✝ + 1 → ((n✝ + 1) * b < (n✝ + 1) * c ↔ b < c)
a0 : 0 < n✝ + 1 + 1
⊢ (n✝ + 1 + 1) * b < (n✝ + 1 + 1) * c ↔ b < c

Proof state:
case succ.succ
b c n✝ : Nat
ih : n✝ * b + b < n✝ * c + c ↔ b < c
⊢ n✝ * b + b + b < n✝ * c + c + c ↔ b < c

Tactic:
omega

Result:
no goals

Proof state:
case succ.succ
b c n✝ : Nat
ih : 0 < n✝ + 1 → ((n✝ + 1) * b < (n✝ + 1) * c ↔ b < c)
a0 : 0 < n✝ + 1 + 1
⊢ (n✝ + 1 + 1) * b < (n✝ + 1 + 1) * c ↔ b < c

Tactic:
simp_all [succ_eq_add_one, Nat.right_distrib]

Result:
case succ.succ
b c n✝ : Nat
ih : n✝ * b + b < n✝ * c + c ↔ b < c
⊢ n✝ * b + b + b < n✝ * c + c + c ↔ b < c

Proof state:
case zero
b c : Nat
a0 : 0 < 0
⊢ 0 * b < 0 * c ↔ b < c

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.zero
b c : Nat
ih : 0 < 0 → (0 * b < 0 * c ↔ b < c)
a0 : 0 < 0 + 1
⊢ (0 + 1) * b < (0 + 1) * c ↔ b < c

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
/-- If `P` is local at the source, local at the target and is stable under post-composition with
open immersions, then `P` can be checked locally around points. -/
lemma iff_exists_resLE [IsLocalAtTarget P] [P.RespectsRight @IsOpenImmersion] :
    P f ↔ ∀ x : X, ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.1) (e : V ≤ f ⁻¹ᵁ U),
      P (f.resLE U V e)

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⊤ ≤ ⨆ x, V x

Tactic:
rintro x -

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(⨆ x, V x)

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⨆ x, V x = ⊤

Tactic:
rw [eq_top_iff]

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⊤ ≤ ⨆ x, V x
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma Icc_isBoundaryPoint_bot : (𝓡∂ 1).IsBoundaryPoint (⊥ : Set.Icc x y)

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ (𝓡∂ 1).IsBoundaryPoint ⊥

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
  Icc_chartedSpaceChartAt_of_le_top (by norm_num [hxy.out])]

Result:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑⊥ < y

Tactic:
norm_num [hxy.out]

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
exact IccLeftChart_extend_bot_mem_frontier

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem ordConnected_iff_upperClosure_inter_lowerClosure :
    s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ (↑(upperClosure s) ∩ ↑(lowerClosure s)).OrdConnected

Tactic:
exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ s.OrdConnected

Tactic:
rw [← h]

Result:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ (↑(upperClosure s) ∩ ↑(lowerClosure s)).OrdConnected

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

Tactic:
refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩

Result:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ s.OrdConnected
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem of_not_mixedCharZero [CharZero R] (h : ∀ p > 0, ¬MixedCharZero R p) :
    ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
case intro.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hp : CharP (R ⧸ I) 0
⊢ CharP (R ⧸ I) 0

Tactic:
exact hp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
intro I hI_ne_top

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero (R ⧸ I)

Proof state:
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (p + 1)
⊢ CharP (R ⧸ I) 0

Tactic:
have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩

Result:
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (p + 1)
h_mixed : MixedCharZero R p.succ
⊢ CharP (R ⧸ I) 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero (R ⧸ I)

Tactic:
suffices CharP (R ⧸ I) 0 from CharP.charP_to_charZero _

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP (R ⧸ I) 0

Proof state:
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (p + 1)
h_mixed : MixedCharZero R p.succ
⊢ CharP (R ⧸ I) 0

Tactic:
exact absurd h_mixed (h p.succ p.succ_pos)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP (R ⧸ I) 0

Tactic:
cases CharP.exists (R ⧸ I) with
| intro p hp =>
  cases p with
  | zero => exact hp
  | succ p =>
    have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
    exact absurd h_mixed (h p.succ p.succ_pos)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0

Tactic:
cases p with
| zero => exact hp
| succ p =>
  have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
  exact absurd h_mixed (h p.succ p.succ_pos)

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ spinGroup Q) : star x ∈ spinGroup Q

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ even Q

Tactic:
dsimp only [CliffordAlgebra.even] at hx₂ ⊢

Result:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯
⊢ star x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯
⊢ star x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯

Tactic:
simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢

Result:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ evenOdd Q 0
⊢ star x ∈ evenOdd Q 0

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Tactic:
refine ⟨pinGroup.star_mem hx₁, ?_⟩

Result:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ even Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : x ∈ pinGroup Q ∧ x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Tactic:
obtain ⟨hx₁, hx₂⟩ := hx

Result:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : x ∈ spinGroup Q
⊢ star x ∈ spinGroup Q

Tactic:
rw [mem_iff] at hx ⊢

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : x ∈ pinGroup Q ∧ x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ evenOdd Q 0
⊢ star x ∈ evenOdd Q 0

Tactic:
simp only [star_def, reverse_mem_evenOdd_iff, involute_mem_evenOdd_iff, hx₂]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem top_add_iff_ne_bot {x : EReal} : ⊤ + x = ⊤ ↔ x ≠ ⊥

Proof state:
x : EReal
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥

Tactic:
constructor <;> intro h

Result:
case mp
x : EReal
h : ⊤ + x = ⊤
⊢ x ≠ ⊥

case mpr
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Proof state:
case mp
x : EReal
h : ⊤ + x = ⊤
⊢ x ≠ ⊥

Tactic:
rintro rfl

Result:
case mp
h : ⊤ + ⊥ = ⊤
⊢ False

Proof state:
case mpr
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
cases x with
| h_bot => contradiction
| h_top => rfl
| h_real r => exact top_add_of_ne_bot h

Result:
no goals

Proof state:
case mpr.h_real
r : ℝ
h : ↑r ≠ ⊥
⊢ ⊤ + ↑r = ⊤

Tactic:
exact top_add_of_ne_bot h

Result:
no goals

Proof state:
case mpr.h_bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

Tactic:
contradiction

Result:
no goals

Proof state:
case mp
h : ⊤ + ⊥ = ⊤
⊢ False

Tactic:
rw [add_bot] at h

Result:
case mp
h : ⊥ = ⊤
⊢ False

Proof state:
case mpr.h_top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case mp
h : ⊥ = ⊤
⊢ False

Tactic:
exact bot_ne_top h

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
lemma nhdsSet_le : 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f : Filter X
s : Set X
⊢ 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Tactic:
simp [nhdsSet]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem disjoint_normalizedFactors {a b : R} (hc : IsCoprime a b) :
    Disjoint (normalizedFactors a) (normalizedFactors b)

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
⊢ False

Tactic:
have xp := prime_of_normalized_factor x hxa

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
xp : Prime x
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
⊢ False

Tactic:
have x_dvd_a := dvd_of_mem_normalizedFactors hxa

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
⊢ False

Tactic:
have x_dvd_b := dvd_of_mem_normalizedFactors hxb

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ Disjoint (normalizedFactors a) (normalizedFactors b)

Tactic:
rw [Multiset.disjoint_left]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ ∀ {a_1 : R}, a_1 ∈ normalizedFactors a → a_1 ∉ normalizedFactors b

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ ∀ {a_1 : R}, a_1 ∈ normalizedFactors a → a_1 ∉ normalizedFactors b

Tactic:
intro x hxa hxb

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
⊢ False

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
x : R
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
xp : Prime x
⊢ False

Tactic:
exact xp.not_unit (hc.isUnit_of_dvd' x_dvd_a x_dvd_b)

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma linearMap_eq_zero_iff_of_eq_span {V : Submodule R M} (f : V →ₗ[R] N)
    {S : Set M} (hV : V = span R S) :
    f = 0 ↔ ∀ (s : S), f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ = 0 :=
  linearMap_eq_iff_of_eq_span f 0 hV

Proof state:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x : M
p p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
F : Type u_8
inst✝³ : FunLike F M M₂
inst✝² : SemilinearMapClass F σ₁₂ M M₂
s✝ t : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ V

Tactic:
simpa only [hV] using subset_span (by simp)

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
x : M
p p' : Submodule R M
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
F : Type u_8
inst✝³ : FunLike F M M₂
inst✝² : SemilinearMapClass F σ₁₂ M M₂
s✝ t : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ S

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem range_eq_map (f : R →ₙ+* S) : f.range = NonUnitalSubring.map f ⊤

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ f.range = NonUnitalSubring.map f ⊤

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_injective2 {p : Fin (n + 1)} :
    Function.Injective2 (@insertNth n α p) := fun xₚ yₚ x y h ↦
  ⟨by simpa using congr_fun h p, funext fun i ↦ by simpa using congr_fun h (succAbove p i)⟩

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (succAbove p i)

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
⊢ xₚ = yₚ

Tactic:
simpa using congr_fun h p

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_update_apply (p : R[X]) (n : ℕ) (a : R) (i : ℕ) :
    (p.update n a).coeff i = if i = n then a else p.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
⊢ (p.update n a).coeff i = if i = n then a else p.coeff i

Tactic:
rw [coeff_update, Function.update_apply]

Result:
no goals