harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_add_add_add_map (x y z : M) :
    Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Proof state:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
rw [add_comm z x]

Result:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Result:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Proof state:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q x + Q y + (B x) y + Q z + ((B x) z + (B y) z) + (Q x + Q y + Q z) =
    Q x + Q y + (B x) y + (Q y + Q z + (B y) z) + (Q x + Q z + (B x) z)

Tactic:
abel

Result:
no goals

Proof state:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)

Tactic:
simp only [h, LinearMap.map_add₂]

Result:
case intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q x + Q y + (B x) y + Q z + ((B x) z + (B y) z) + (Q x + Q y + Q z) =
    Q x + Q y + (B x) y + (Q y + Q z + (B y) z) + (Q x + Q z + (B x) z)
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.card_neighborFinset_union_eq {v w : V} (h : G.IsSRGWith n k ℓ μ) :
    #(G.neighborFinset v ∪ G.neighborFinset w) =
      2 * k - Fintype.card (G.commonNeighbors v w)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)

Tactic:
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card ↑(G.commonNeighbors v w) =
    2 * k - Fintype.card ↑(G.commonNeighbors v w) + Fintype.card ↑(G.commonNeighbors v w)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Tactic:
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ G.degree v ≤ 2 * k

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ G.degree v ≤ 2 * k

Tactic:
simp [h.regular.degree_eq, two_mul]

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card ↑(G.commonNeighbors v w) =
    2 * k - Fintype.card ↑(G.commonNeighbors v w) + Fintype.card ↑(G.commonNeighbors v w)

Tactic:
rw [Nat.sub_add_cancel, ← Set.toFinset_card]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k

Tactic:
simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter,
  h.regular.degree_eq, two_mul]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem tanh_half_dist (z w : ℍ) :
    tanh (dist z w / 2) = dist (z : ℂ) w / dist (z : ℂ) (conj ↑w)

Proof state:
z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
z w : ℍ
⊢ tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_half_dist, cosh_half_dist, div_div_div_comm, div_self, div_one]

Result:
z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_modify (h : m.1.WF) {k k' : α} {f : β → β} :
    (Const.modify m k f).contains k' = m.contains k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
⊢ (modify m k f).contains k' = m.contains k'

Tactic:
simp_to_model [Const.modify] using List.Const.containsKey_modifyKey

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean
theorem of_iso {P Q : C} (i : P ≅ Q) (hP : Injective P) : Injective Q :=
  {
    factors := fun g f mono => by
      obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono
      refine ⟨h ≫ i.hom, ?_⟩
      rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id] }

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g

Tactic:
rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g

Tactic:
refine ⟨h ≫ i.hom, ?_⟩

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toLinearMap₂'_apply' {T : Type*} [CommSemiring T] (M : Matrix n m T) (v : n → T)
    (w : m → T) : Matrix.toLinearMap₂' T M v w = dotProduct v (M *ᵥ w)

Proof state:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ ∑ i : n, ∑ j : m, v i •> w j •> M i j = ∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Result:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ •> w j •> M x✝¹ j = v x✝¹ * ∑ x : m, M x✝¹ x * w x

Proof state:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ •> w j •> M x✝¹ j = v x✝¹ * ∑ x : m, M x✝¹ x * w x

Tactic:
rw [Finset.mul_sum]

Result:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ •> w j •> M x✝¹ j = ∑ i : m, v x✝¹ * (M x✝¹ i * w i)

Proof state:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ •> w x✝¹ •> M x✝³ x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]

Result:
no goals

Proof state:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ (((toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w

Tactic:
simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]

Result:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ ∑ i : n, ∑ j : m, v i •> w j •> M i j = ∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1

Proof state:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j : m, v x✝¹ •> w j •> M x✝¹ j = ∑ i : m, v x✝¹ * (M x✝¹ i * w i)

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Result:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ •> w x✝¹ •> M x✝³ x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
-- Mathlib/Algebra/Module/CharacterModule.lean
protected lemma int.divByNat_self (n : ℕ) :
    int.divByNat n n = 0

Proof state:
case inl

⊢ (int.divByNat 0) ↑0 = 0

Tactic:
apply map_zero

Result:
no goals

Proof state:
n : ℕ
⊢ (int.divByNat n) ↑n = 0

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Result:
case inl

⊢ (int.divByNat 0) ↑0 = 0

case inr
n : ℕ
h0 : n ≠ 0
⊢ (int.divByNat n) ↑n = 0

Proof state:
case inr
n : ℕ
h0 : n ≠ 0
⊢ (int.divByNat n) ↑n = 0

Tactic:
exact (AddCircle.coe_eq_zero_iff _).mpr
  ⟨1, by simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]⟩

Result:
no goals

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ 1 • 1 = (fun x => LinearMap.id ↑n • x) (↑n)⁻¹

Tactic:
simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma lift_lt_comp : lift a < comp b ↔ Disjoint a b := ⟨by rintro ⟨_⟩; assumption, LT.sep⟩

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a < comp b → Disjoint a b

Tactic:
rintro ⟨_⟩

Result:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b

Proof state:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b

Tactic:
assumption

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem snd_comp_quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.snd _ _).comp
        (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor inf_le_right

Proof state:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
apply Quotient.ringHom_ext

Result:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Tactic:
ext

Result:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝

Proof state:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem fst_comp_toProd : (MonoidHom.fst M N).comp toProd = fst

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.fst M N).comp toProd = fst

Tactic:
rw [← fst_prod_snd, MonoidHom.fst_comp_prod]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
lemma isCoprime_col (A : SL(2, R)) (j : Fin 2) : IsCoprime (A 0 j) (A 1 j)

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]

Result:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Defs.lean
@[aesop safe apply (rule_sets := [SetLike])]
lemma nnratCast_mem (s : S) (q : ℚ≥0) : (q : K) ∈ s

Proof state:
K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
⊢ ↑q ∈ s

Tactic:
simpa only [NNRat.cast_def] using div_mem (natCast_mem s q.num) (natCast_mem s q.den)

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma div2_val (n) : div2 n = n / 2

Proof state:
n : ℕ
⊢ n.div2 = n / 2

Tactic:
refine Nat.eq_of_mul_eq_mul_left (by decide)
  (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))

Result:
n : ℕ
⊢ n % 2 + 2 * n.div2 = n

Proof state:
n : ℕ
⊢ n % 2 + 2 * n.div2 = n

Tactic:
rw [mod_two_of_bodd, bodd_add_div2]

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
protected lemma bijective (f : S →+* Q) (hf : f.comp (algebraMap R S) = algebraMap R Q) :
    Function.Bijective f :=
  (show f = IsLocalization.algEquiv M S Q by
    apply IsLocalization.ringHom_ext M; rw [hf]; ext; simp) ▸
    (IsLocalization.algEquiv M S Q).toEquiv.bijective

Proof state:
case h.a
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
x✝ : R
⊢ (algebraMap R Q) x✝ = ((↑(algEquiv M S Q)).comp (algebraMap R S)) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ f = ↑(algEquiv M S Q)

Tactic:
apply IsLocalization.ringHom_ext M

Result:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ f.comp (algebraMap R S) = (↑(algEquiv M S Q)).comp (algebraMap R S)

Proof state:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)

Tactic:
ext

Result:
case h.a
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
x✝ : R
⊢ (algebraMap R Q) x✝ = ((↑(algEquiv M S Q)).comp (algebraMap R S)) x✝

Proof state:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ f.comp (algebraMap R S) = (↑(algEquiv M S Q)).comp (algebraMap R S)

Tactic:
rw [hf]

Result:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)
-- Mathlib/Topology/Instances/AddCircle.lean
lemma toAddCircle_natCast (j : ℕ) :
    toAddCircle (j : ZMod N) = ↑(j / N : ℝ)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℕ
⊢ toAddCircle ↑j = ↑(↑j / ↑N)

Tactic:
simpa using toAddCircle_intCast (N := N) j

Result:
no goals
-- Mathlib/Order/Monotone/Monovary.lean
lemma antivaryOn_iff_antivary : AntivaryOn f g s ↔ Antivary (fun i : s ↦ f i) fun i ↦ g i

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ Antivary (fun i => f ↑i) fun i => g ↑i

Tactic:
simp [Antivary, AntivaryOn]

Result:
no goals
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_aux4 (n : ℕ) :
    (p : 𝕄) ^ (n + 1) * wittMul p (n + 1) =
    -((p : 𝕄) ^ (n + 1) * X (0, n + 1)) * ((p : 𝕄) ^ (n + 1) * X (1, n + 1)) +
    (p : 𝕄) ^ (n + 1) * X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
    (p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
    (remainder p n - wittPolyProdRemainder p (n + 1))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n

Tactic:
exact mul_polyOfInterest_aux3 _ _

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      (remainder p n - wittPolyProdRemainder p (n + 1))

Tactic:
rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_centroidWeights_eq_one_of_card_ne_zero [CharZero k] (h : #s ≠ 0) :
    ∑ i ∈ s, s.centroidWeights k i = 1

Proof state:
k : Type u_1
inst✝¹ : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
h : #s ≠ 0
⊢ ↑(#s) * (↑(#s))⁻¹ = 1

Tactic:
refine mul_inv_cancel₀ ?_

Result:
k : Type u_1
inst✝¹ : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
h : #s ≠ 0
⊢ ↑(#s) ≠ 0

Proof state:
k : Type u_1
inst✝¹ : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
h : #s ≠ 0
⊢ ↑(#s) ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
h : #s ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
simp only [centroidWeights_apply, sum_const, nsmul_eq_mul, ne_eq, Nat.cast_eq_zero, card_eq_zero]

Result:
k : Type u_1
inst✝¹ : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
h : #s ≠ 0
⊢ ↑(#s) * (↑(#s))⁻¹ = 1
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.tensorProductTo_surjective :
    Function.Surjective (KaehlerDifferential.D R S).tensorProductTo

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : Ω[S⁄R]
⊢ ∃ a, (D R S).tensorProductTo a = x

Tactic:
obtain ⟨x, rfl⟩ := (KaehlerDifferential.ideal R S).toCotangent_surjective x

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ ∃ a, (D R S).tensorProductTo a = (ideal R S).toCotangent x

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ ∃ a, (D R S).tensorProductTo a = (ideal R S).toCotangent x

Tactic:
exact ⟨x, KaehlerDifferential.D_tensorProductTo x⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Surjective ⇑(D R S).tensorProductTo

Tactic:
intro x

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : Ω[S⁄R]
⊢ ∃ a, (D R S).tensorProductTo a = x