harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Fix.rec_unique {α : Type u} (g : F α → α) (h : Fix F → α)
    (hyp : ∀ x, h (Fix.mk x) = g (h <$> x)) : Fix.rec g = h

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
⊢ rec g = h

Tactic:
ext x

Result:
case h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x

Proof state:
case h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x

Tactic:
apply Fix.ind_rec

Result:
case h.h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)

Proof state:
case h.h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = h (mk x)

Tactic:
rw [hyp, ← hyp', Fix.rec_eq]

Result:
no goals

Proof state:
case h.h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)

Tactic:
intro x hyp'

Result:
case h.h
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = h (mk x)
-- Mathlib/RingTheory/Algebraic/Defs.lean
theorem Subalgebra.isAlgebraic_iff (S : Subalgebra R A) :
    S.IsAlgebraic ↔ Algebra.IsAlgebraic R S

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ x ∈ S, _root_.IsAlgebraic R x) ↔ Algebra.IsAlgebraic R ↥S

Tactic:
rw [Subtype.forall', Algebra.isAlgebraic_def]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), _root_.IsAlgebraic R x

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥S

Tactic:
delta Subalgebra.IsAlgebraic

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ x ∈ S, _root_.IsAlgebraic R x) ↔ Algebra.IsAlgebraic R ↥S

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0

Tactic:
have h : Function.Injective S.val := Subtype.val_injective

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ S.val ((aeval x) p) = 0

Tactic:
rw [← aeval_algHom_apply, S.val_apply]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), _root_.IsAlgebraic R x

Tactic:
refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0

Tactic:
conv_rhs => rw [← h.eq_iff, map_zero]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ S.val ((aeval x) p) = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_insert [@TransCmp α cmp] {t : RBNode α} (ht : Balanced t c n) (ht₂ : Ordered cmp t) :
    v' ∈ t.insert cmp v ↔ (v' ∈ t ∧ t.find? (cmp v) ≠ some v') ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
h : v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ v' ∈ t ∧ find? (cmp v) t ≠ some v'

Tactic:
simp [← mem_toList, h₁, h]

Result:
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
p : Path α
e : zoom (cmp v) t = (nil, p)
w✝¹ w✝ : List α
h₁ : t.toList = w✝¹ ++ w✝
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h✝ : (v' ∈ w✝¹ ∨ v' ∈ w✝) ∨ v' = v
h : v' ∈ w✝¹ ∨ v' ∈ w✝
⊢ ¬find? (cmp v) t = some v'

Proof state:
case inr.refl
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ r✝ : RBNode α
p : Path α
w✝¹ w✝ : List α
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' ∈ w✝
e : zoom (cmp v) t = (node c✝ l✝ v' r✝, p)
h₁ : t.toList = w✝¹ ++ v' :: w✝
⊢ cmpLT cmp v' v'

Tactic:
have := ht₂.toList_sorted

Result:
case inr.refl
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
c✝ : RBColor
l✝ r✝ : RBNode α
p : Path α
w✝¹ w✝ : List α
h₂ : (insert cmp t v).toList = w✝¹ ++ v :: w✝
h : v' ∈ w✝¹ ∨ v' ∈ w✝
e : zoom (cmp v) t = (node c✝ l✝ v' r✝, p)
h₁ : t.toList = w✝¹ ++ v' :: w✝
this : List.Pairwise (cmpLT cmp) t.toList
⊢ cmpLT cmp v' v'

Proof state:
case refine_3
α : Type u_1
cmp : α → α → Ordering
c : RBColor
n : Nat
v v' : α
inst✝ : TransCmp cmp
t : RBNode α
ht : t.Balanced c n
ht₂ : Ordered cmp t
h : v' = v
⊢ v' ∈ insert cmp t v

Tactic:
exact h ▸ mem_insert_self ht

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
/-- Right unitality of the enriched structure -/
@[reassoc (attr := simp)]
lemma comp_id (x y : C) [Closed x] [Closed y] :
    (ρ_ ((ihom x).obj y)).inv ≫ _ ◁ id y ≫ comp x y y = 𝟙 _

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
rw [← uncurry_natural_left]

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ uncurry ((ρ_ ((ihom x).obj y)).inv ≫ (ihom x).obj y ◁ id y ≫ comp x y y) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, compTranspose_eq,
  associator_inv_naturality_right_assoc, ← rightUnitor_tensor_inv_assoc,
  whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc, ← uncurry_id_eq_ev y y]

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) =
    uncurry (𝟙 ((ihom x).obj y))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ρ_ ((ihom x).obj y)).inv ≫ (ihom x).obj y ◁ id y ≫ comp x y y = 𝟙 ((ihom x).obj y)

Tactic:
apply uncurry_injective

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ uncurry ((ρ_ ((ihom x).obj y)).inv ≫ (ihom x).obj y ◁ id y ≫ comp x y y) = uncurry (𝟙 ((ihom x).obj y))

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
simp only [Functor.id_obj]

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
simp [id_eq, uncurry_id_eq_ev]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_closure_iff_exists_list {R} [Semiring R] {s : Set R} {x} :
    x ∈ closure s ↔ ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map List.prod).sum = x

Proof state:
case mp.one
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩

Result:
no goals

Proof state:
case mp.mul
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y

Tactic:
obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM

Result:
case mp.mul.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_multiset_count_of_subset [DecidableEq α] [CommMonoid α] (m : Multiset α) (s : Finset α)
    (hs : m.toFinset ⊆ s) : m.prod = ∏ i ∈ s, i ^ m.count i

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
⊢ m.toFinset ⊆ s → m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
refine Quot.induction_on m fun l => ?_

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset (Quot.mk (⇑(isSetoid α)) l) ⊆ s →
    Multiset.prod (Quot.mk (⇑(isSetoid α)) l) = ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid α)) l)

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset (Quot.mk (⇑(isSetoid α)) l) ⊆ s →
    Multiset.prod (Quot.mk (⇑(isSetoid α)) l) = ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simp only [quot_mk_to_coe'', prod_coe, coe_count]

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ (↑l).toFinset ⊆ s → l.prod = ∏ x ∈ s, x ^ List.count x l

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
revert hs

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
⊢ m.toFinset ⊆ s → m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ (↑l).toFinset ⊆ s → l.prod = ∏ x ∈ s, x ^ List.count x l

Tactic:
apply prod_list_count_of_subset l s

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective
    (hm : Injective (rTensor N (span R (Set.range m)).subtype))
    (hmn : ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N)) : VanishesTrivially R m n

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
hm' : span R (Set.range m') = ⊤
hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0
this : ∃ k a y, (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧ ∀ (j : Fin k), ∑ i : ι, a i j • m' i = 0
⊢ ∃ k a y, (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧ ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0

Tactic:
convert this with κ _ a y j

Result:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
hm' : span R (Set.range m') = ⊤
hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0
this : ∃ k a y, (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧ ∀ (j : Fin k), ∑ i : ι, a i j • m' i = 0
κ : ℕ
x✝ : ι → Fin κ → R
a : Fin κ → N
y : Fin κ
⊢ ∑ i : ι, x✝ i y • m i = 0 ↔ ∑ i : ι, x✝ i y • m' i = 0

Proof state:
case a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
⊢ Submodule.map (span R (Set.range m)).subtype (span R (Set.range m')) = Submodule.map (span R (Set.range m)).subtype ⊤

Tactic:
rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]

Result:
case a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
⊢ span R (Set.range (Subtype.val ∘ m')) = span R (Set.range m)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
    (f : β → β) : Const.modify m a f = Const.modifyₘ m a f

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
⊢ modify m a f = modifyₘ m a f

Tactic:
rw [modify_eq_alter, alter_eq_alterₘ, modifyₘ]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Continuous.lean
theorem _root_.isBoundedBilinearMap_inner [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] :
    IsBoundedBilinearMap ℝ fun p : E × E => ⟪p.1, p.2⟫ :=
  { add_left := inner_add_left
    smul_left := fun r x y => by
      simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]
    add_right := inner_add_right
    smul_right := fun r x y => by
      simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]
    bound :=
      ⟨1, zero_lt_one, fun x y => by
        rw [one_mul]
        exact norm_inner_le_norm x y⟩ }

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖inner (x, y).1 (x, y).2‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
rw [one_mul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖inner (x, y).1 (x, y).2‖ ≤ ‖x‖ * ‖y‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
r : ℝ
x y : E
⊢ inner (x, r • y).1 (x, r • y).2 = r • inner (x, y).1 (x, y).2

Tactic:
simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖inner (x, y).1 (x, y).2‖ ≤ ‖x‖ * ‖y‖

Tactic:
exact norm_inner_le_norm x y

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
r : ℝ
x y : E
⊢ inner (r • x, y).1 (r • x, y).2 = r • inner (x, y).1 (x, y).2

Tactic:
simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem is_ideal_adic_pow {J : Ideal R} (h : IsAdic J) {n : ℕ} (hn : 0 < n) : IsAdic (J ^ n)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ (∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)) ∧ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)

case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_spec [NeZero n] (x : ZMod n) (y : ℤ) :
    x.valMinAbs = y ↔ x = y ∧ y * 2 ∈ Set.Ioc (-n : ℤ) n where
  mp

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩

Result:
no goals

Proof state:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y

Tactic:
rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]

Result:
no goals

Proof state:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| * |2| < ↑n * 2

Tactic:
rw [← abs_mul, sub_mul, abs_lt]

Result:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs - y = 0

Tactic:
apply @Int.eq_zero_of_abs_lt_dvd n

Result:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y

case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| < ↑n

Proof state:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| < ↑n

Tactic:
rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)]

Result:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| * 2 < ↑n * 2

Proof state:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| * 2 < ↑n * 2

Tactic:
nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]

Result:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| * |2| < ↑n * 2

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs = y

Tactic:
rw [← sub_eq_zero]

Result:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs - y = 0

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
⊢ x.valMinAbs = y → x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
rintro rfl

Result:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

Proof state:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2

Tactic:
constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun a b => f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
exact image_image2_distrib fun _ _ => h_antidistrib _ _

Result:
no goals

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
rw [image2_swap f]

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun a b => f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)
-- Mathlib/ModelTheory/Types.lean
theorem toList_foldr_inf_mem {p : T.CompleteType α} {t : Finset (L[[α]]).Sentence} :
    t.toList.foldr (· ⊓ ·) ⊤ ∈ p ↔ (t : L[[α]].Theory) ⊆ ↑p

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p

Tactic:
simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff,
  Sentence.Realize, Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]

Result:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ (∀ (M : ModelType ↑p), ∀ φ ∈ t, φ.Realize default default) ↔
    ∀ x ∈ ↑t, ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ (∀ (M : ModelType ↑p), ∀ φ ∈ t, φ.Realize default default) ↔
    ∀ x ∈ ↑t, ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default

Tactic:
exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩

Result:
no goals