harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[reassoc]
lemma app_shift (a : A) (X : C) :
    τ.app (X⟦a⟧) = (F₁.commShiftIso a).hom.app X ≫ (τ.app X)⟦a⟧' ≫
      (F₂.commShiftIso a).inv.app X

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_7, u_1} C
inst✝⁶ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ τ.app ((shiftFunctor C a).obj X) =
    (F₁.commShiftIso a).hom.app X ≫ (shiftFunctor D a).map (τ.app X) ≫ (F₂.commShiftIso a).inv.app X

Tactic:
simp [shift_app_comm_assoc τ a X]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem revzip_powersetAux_perm_aux' {l : List α} :
    revzip (powersetAux l) ~ revzip (powersetAux' l)

Proof state:
α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']

Result:
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l - x)) (powersetAux l) ~ List.map (fun x => (x, ↑l - x)) (powersetAux' l)

Proof state:
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l - x)) (powersetAux l) ~ List.map (fun x => (x, ↑l - x)) (powersetAux' l)

Tactic:
exact powersetAux_perm_powersetAux'.map _

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algEquiv_apply {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
    algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
⊢ (algEquiv hx h_mp) (AdjoinSimple.gen K x) = AdjoinSimple.gen K y

Tactic:
have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ (algEquiv hx h_mp) (AdjoinSimple.gen K x) = AdjoinSimple.gen K y

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ (algEquiv hx h_mp) (AdjoinSimple.gen K x) = AdjoinSimple.gen K y

Tactic:
rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral,
  symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_apply_root,
  adjoinRootEquivAdjoin_apply_root K hy.isIntegral]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_map {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
    Perm (toListModel (m.map f).1.buckets)
      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → δ a
⊢ toListModel (map f m).val.buckets ~ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets)

Tactic:
rw [map_eq_mapₘ]

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → δ a
⊢ toListModel (m.mapₘ f).val.buckets ~ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → δ a
⊢ toListModel (m.mapₘ f).val.buckets ~ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets)

Tactic:
exact toListModel_mapₘ

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_eq_finrank_of_isSeparable [Algebra.IsSeparable F E] :
    finSepDegree F E = finrank F E

Proof state:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(restrictScalars F M) = finrank F ↥(restrictScalars F M)

Tactic:
have := Algebra.IsAlgebraic.of_finite L M

Result:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M
this : Algebra.IsAlgebraic ↥L ↥M
⊢ finSepDegree F ↥(restrictScalars F M) = finrank F ↥(restrictScalars F M)
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp)]
lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f where
  bijOn := bijOn_empty _
  map_prod_eq_map_prod s t hs ht

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
f : α → β
n : ℕ
s t : Multiset α
hs : ∀ ⦃x : α⦄, x ∈ s → x ∈ ∅
ht : ∀ ⦃x : α⦄, x ∈ t → x ∈ ∅
⊢ s.card = n → t.card = n → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
simp [eq_zero_of_forall_not_mem hs, eq_zero_of_forall_not_mem ht]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@[simp]
lemma natTrailingDegree_X_pow (n : ℕ) :
    (X ^ n : R[X]).natTrailingDegree = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).natTrailingDegree = n

Tactic:
rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma isTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n,
      (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case h.inr.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
apply det_zero_of_column_eq hij

Result:
case h.inr.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ ∀ (k_1 : Fin k), A.submatrix f g k_1 i = A.submatrix f g k_1 j
-- Mathlib/Topology/CompactOpen.lean
@[norm_cast]
lemma inseparable_coe {f g : C(X, Y)} : Inseparable (f : X → Y) g ↔ Inseparable f g

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
⊢ Inseparable ⇑f ⇑g ↔ Inseparable f g

Tactic:
simp only [inseparable_iff_specializes_and, specializes_coe]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_verschiebung_coeff_eq_zero (x : 𝕎 R) {n : ℕ} {m : ℕ} (h : m < n) :
    (verschiebung^[n] x).coeff m = 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n m : ℕ
h : m < n
⊢ ((⇑verschiebung)^[n] x).coeff m = 0

Tactic:
induction' n with n ih generalizing m

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
m : ℕ
h : m < 0
⊢ ((⇑verschiebung)^[0] x).coeff m = 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ ((⇑verschiebung)^[n + 1] x).coeff m = 0

Proof state:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff (m' + 1) = 0

Tactic:
rw [verschiebung_coeff_succ, ih]

Result:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff m = 0

Tactic:
cases m with
| zero => exact verschiebung_coeff_zero _
| succ m' =>
  rw [verschiebung_coeff_succ, ih]
  simpa using h

Result:
no goals

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ ((⇑verschiebung)^[n + 1] x).coeff m = 0

Tactic:
rw [iterate_succ_apply']

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff m = 0

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
m : ℕ
h : m < 0
⊢ ((⇑verschiebung)^[0] x).coeff m = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Tactic:
simpa using h

Result:
no goals

Proof state:
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
h : 0 < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff 0 = 0

Tactic:
exact verschiebung_coeff_zero _

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_add_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
    term (f + g) s n = term f s n + term g s n

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f + g) s n = term f s n + term g s n

Tactic:
simp [term_add]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem unitCoeff_spec {x : ℤ_[p]} (hx : x ≠ 0) :
    x = (unitCoeff hx : ℤ_[p]) * (p : ℤ_[p]) ^ x.valuation

Proof state:
case a.ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0

Tactic:
exact NeZero.ne _

Result:
no goals

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ x.valuation

Tactic:
rw [unitCoeff_coe, mul_assoc, ← zpow_natCast, ← zpow_add₀]

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-↑x.valuation + ↑x.valuation)

case a.ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-↑x.valuation + ↑x.valuation)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ x = ↑(unitCoeff hx) * ↑p ^ x.valuation

Tactic:
apply Subtype.coe_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ x.valuation)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ x.valuation)

Tactic:
push_cast

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ x.valuation
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
theorem map_smul_right (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g

Proof state:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝

Tactic:
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
  smul_apply, tmul_smul]

Result:
no goals

Proof state:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map f (r • g) = r • map f g

Tactic:
ext

Result:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
theorem _root_.separatingDual_iff_injective : SeparatingDual R V ↔
    Function.Injective (ContinuousLinearMap.coeLM (R := R) R (M := V) (N₃ := R)).flip

Proof state:
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
⊢ SeparatingDual R V ↔ Function.Injective ⇑(ContinuousLinearMap.coeLM R).flip

Tactic:
simp_rw [separatingDual_def, Ne, injective_iff_map_eq_zero]

Result:
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
⊢ (∀ (x : V), ¬x = 0 → ∃ f, ¬f x = 0) ↔ ∀ (a : V), (ContinuousLinearMap.coeLM R).flip a = 0 → a = 0

Proof state:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (¬v = 0 → ∃ f, ¬f v = 0) ↔ (ContinuousLinearMap.coeLM R).flip v = 0 → v = 0

Tactic:
rw [not_imp_comm, LinearMap.ext_iff]

Result:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (¬∃ f, ¬f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0

Proof state:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (∀ (f : V →L[R] R), f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (¬∃ f, ¬f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0

Tactic:
push_neg

Result:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (∀ (f : V →L[R] R), f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
⊢ (∀ (x : V), ¬x = 0 → ∃ f, ¬f x = 0) ↔ ∀ (a : V), (ContinuousLinearMap.coeLM R).flip a = 0 → a = 0

Tactic:
congrm ∀ v, ?_

Result:
case a
R : Type u_1
V : Type u_2
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalRing R
inst✝ : Module R V
v : V
⊢ (¬v = 0 → ∃ f, ¬f v = 0) ↔ (ContinuousLinearMap.coeLM R).flip v = 0 → v = 0
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f

Proof state:
case h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x✝¹ x✝ : E
⊢ (fderivWithin 𝕜 f univ x✝¹) x✝ = (fderiv 𝕜 f x✝¹) x✝

Tactic:
rw [fderiv]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
⊢ fderivWithin 𝕜 f univ = fderiv 𝕜 f

Tactic:
ext

Result:
case h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x✝¹ x✝ : E
⊢ (fderivWithin 𝕜 f univ x✝¹) x✝ = (fderiv 𝕜 f x✝¹) x✝
-- Mathlib/Topology/Bases.lean
theorem secondCountableTopology_induced (α β) [t : TopologicalSpace β] [SecondCountableTopology β]
    (f : α → β) : @SecondCountableTopology α (t.induced f)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
⊢ SecondCountableTopology α

Tactic:
letI := t.induced f

Result:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α

Tactic:
rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
⊢ SecondCountableTopology α

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α

Tactic:
refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }

Result:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)

Tactic:
rw [eq, induced_generateFrom_eq]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_mkQ_single_mul (x y z) :
    (z𝖣x * y) = ((z * x)𝖣y) + (z * y)𝖣x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S

Tactic:
simp_rw [← Finsupp.smul_single_one _ z, ← @smul_eq_mul _ _ z, ← Finsupp.smul_single, ← smul_add,
  ← smul_sub]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single y x + single x y - single (x * y) 1) ∈ kerTotal R S

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single y x + single x y - single (x * y) 1) ∈ kerTotal R S

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inr <| ⟨⟨_, _⟩, rfl⟩))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ (z𝖣x * y) = ((z * x)𝖣y) + (z * y)𝖣x

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
  Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S
-- Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
/--
If `s` is a spanning set of `Γ(X, U)`, such that each `X.basicOpen i` is affine, then `U` is also
affine.
-/
lemma isAffineOpen_of_isAffineOpen_basicOpen (U) (s : Set Γ(X, U))
    (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) :
    IsAffineOpen U

Proof state:
case hs₂.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen
    (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) ((ConcreteCategory.hom U.topIso.inv) j)))

Tactic:
simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ IsAffineOpen U

Tactic:
apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)

Result:
case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.span (⇑(ConcreteCategory.hom U.topIso.inv) '' s) = ⊤

case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom U.topIso.inv) '' s, IsAffineOpen ((↑U).basicOpen i)

Proof state:
case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom U.topIso.inv) '' s, IsAffineOpen ((↑U).basicOpen i)

Tactic:
rintro _ ⟨j, hj, rfl⟩

Result:
case hs₂.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen ((↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) j))

Proof state:
case hs₂.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen ((↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) j))

Tactic:
rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]

Result:
case hs₂.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen
    (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) ((ConcreteCategory.hom U.topIso.inv) j)))

Proof state:
case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.span (⇑(ConcreteCategory.hom U.topIso.inv) '' s) = ⊤

Tactic:
rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]

Result:
no goals