harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma comp_left_inv (C : VariableChange R) : comp (inv C) C = id

Proof state:
case s
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

Tactic:
linear_combination -C.s * C.u.inv_mul

Result:
no goals

Proof state:
case r
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0

Tactic:
linear_combination -C.r * pow_mul_pow_eq_one 2 C.u.inv_mul

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
          C.r,
      s :=
        ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s + C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
              ↑C.u ^ 2 +
          C.t } =
    { u := 1, r := 0, s := 0, t := 0 }

Tactic:
ext <;> dsimp only

Result:
case u.a
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ ↑(C.u⁻¹ * C.u) = ↑1

case r
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0

case s
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

case t
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0

Proof state:
case u.a
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ ↑(C.u⁻¹ * C.u) = ↑1

Tactic:
exact C.u.inv_mul

Result:
no goals

Proof state:
case t
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0

Tactic:
linear_combination (C.r * C.s - C.t) * pow_mul_pow_eq_one 3 C.u.inv_mul
  + -C.r * C.s * pow_mul_pow_eq_one 2 C.u.inv_mul

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ C.inv.comp C = id

Tactic:
rw [comp, id, inv]

Result:
R : Type u
inst✝ : CommRing R
C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
          C.r,
      s :=
        ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s + C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
              ↑C.u ^ 2 +
          C.t } =
    { u := 1, r := 0, s := 0, t := 0 }
-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem sum_div_nat_floor_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) :
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
      c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Proof state:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ filter (fun i => j < c ^ i) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
exact sum_div_pow_sq_le_div_sq N hj hc

Result:
no goals

Proof state:
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun i => j < c ^ i) (range N)
⊢ c ^ i ≤ (1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊

Tactic:
rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]

Result:
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun i => j < c ^ i) (range N)
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_orthogonalProjection_of_le {U V : Submodule 𝕜 E}
    [HasOrthogonalProjection U] [HasOrthogonalProjection V] (h : U ≤ V) (x : E) :
    orthogonalProjection U (orthogonalProjection V x) = orthogonalProjection U x :=
  Eq.symm <| by
    simpa only [sub_eq_zero, map_sub] using
      orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
        (Submodule.orthogonal_le h (sub_orthogonalProjection_mem_orthogonal x))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection U
inst✝ : HasOrthogonalProjection V
h : U ≤ V
x : E
⊢ (orthogonalProjection U) x = (orthogonalProjection U) ↑((orthogonalProjection V) x)

Tactic:
simpa only [sub_eq_zero, map_sub] using
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
    (Submodule.orthogonal_le h (sub_orthogonalProjection_mem_orthogonal x))

Result:
no goals
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_coeff_degree_ne {i : ℕ} (hi : p.degree ≠ i) :
    coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
rw [integralNormalization_coeff, if_neg hi]

Result:
no goals
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
/--
In a semisimple Lie algebra,
Lie ideals that are contained in the supremum of a finite collection of atoms
are themselves the supremum of a finite subcollection of those atoms.

By a compactness argument, this statement can be extended to arbitrary sets of atoms.
See `atomistic`.

The proof is by induction on the finite set of atoms.
-/
private
lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal R L | IsAtom I} →
    ∀ I : LieIdeal R L, I ≤ s.sup id → ∃ t ⊆ s, I = t.sup id

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
this : ⟨y, hy⟩ ∈ center R ↥J
⊢ y + z ∈ K

Tactic:
have _inst := isSimple_of_isAtom J (hs hJs)

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
this : ⟨y, hy⟩ ∈ center R ↥J
_inst : IsSimple R ↥J
⊢ y + z ∈ K

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : J ⊓ I = ⊥
⊢ ⁅↑j, y + z⁆ ∈ ⊥

Tactic:
apply this.le

Result:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : J ⊓ I = ⊥
⊢ ⁅↑j, y + z⁆ ∈ J ⊓ I
-- Mathlib/Order/Bounds/Basic.lean
theorem exists_lub_Iio (i : γ) : ∃ j, IsLUB (Iio i) j

Proof state:
case pos.intro.intro
γ : Type v
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩

Result:
no goals

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))

Tactic:
rw [mem_lowerBounds]

Result:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ ∀ x ∈ upperBounds (Iio i), i ≤ x

Proof state:
case pos
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt

Result:
case pos.intro.intro
γ : Type v
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
refine ⟨i, fun j hj => le_of_lt hj, ?_⟩

Result:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ∃ x ∈ upperBounds (Iio i), x < i
⊢ ∃ j ∈ upperBounds (Iio i), j < i

Tactic:
exact h

Result:
no goals

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ ∀ x ∈ upperBounds (Iio i), i ≤ x

Tactic:
by_contra h

Result:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ¬∀ x ∈ upperBounds (Iio i), i ≤ x
⊢ False

Proof state:
γ : Type v
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i

Result:
case pos
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ¬∀ x ∈ upperBounds (Iio i), i ≤ x
⊢ ∃ j ∈ upperBounds (Iio i), j < i

Tactic:
push_neg at h

Result:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ∃ x ∈ upperBounds (Iio i), x < i
⊢ ∃ j ∈ upperBounds (Iio i), j < i

Proof state:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ¬∀ x ∈ upperBounds (Iio i), i ≤ x
⊢ False

Tactic:
refine h_exists_lt ?_

Result:
case neg
γ : Type v
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j ∈ upperBounds (Iio i), j < i
h : ¬∀ x ∈ upperBounds (Iio i), i ≤ x
⊢ ∃ j ∈ upperBounds (Iio i), j < i
-- Mathlib/Algebra/Order/Round.lean
theorem round_le (x : α) (z : ℤ) : |x - round x| ≤ |x - z|

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1

Tactic:
norm_cast

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1

Proof state:
case inl.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ |x - ↑z|

Tactic:
conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]

Result:
case inl.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ fract x + (↑⌊x⌋ - ↑z)

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1

Tactic:
exact floor_le_sub_one_iff.mpr hx

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)

Tactic:
rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
  le_sub_comm]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)

Tactic:
conv_rhs => rw [← fract_add_floor x]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ |x - ↑(round x)| ≤ |x - ↑z|

Tactic:
rw [abs_sub_round_eq_min, min_le_iff]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

Tactic:
rcases le_or_lt (z : α) x with (hx | hx) <;> [left; right]

Result:
case inl.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ |x - ↑z|

case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|

Proof state:
case inl.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ fract x + (↑⌊x⌋ - ↑z)

Tactic:
simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|

Tactic:
rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive] lemma le_mulEnergy : s.card * t.card ≤ Eₘ[s, t]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a : α × α
x✝¹ : a ∈ ↑(s ×ˢ t)
b : α × α
x✝ : b ∈ ↑(s ×ˢ t)
⊢ a.1 = b.1 → a.2 = b.2 → a = b

Tactic:
exact Prod.ext

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s * #t ≤ Eₘ[s, t]

Tactic:
rw [← card_product]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]

Tactic:
refine
  card_le_card_of_injOn (@fun x => ((x.1, x.1), x.2, x.2)) (by simp) fun a _ b _ => ?_

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a : α × α
x✝¹ : a ∈ ↑(s ×ˢ t)
b : α × α
x✝ : b ∈ ↑(s ×ˢ t)
⊢ (fun x => ((x.1, x.1), x.2, x.2)) a = (fun x => ((x.1, x.1), x.2, x.2)) b → a = b

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ a ∈ s ×ˢ t,
    (fun x => ((x.1, x.1), x.2, x.2)) a ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a : α × α
x✝¹ : a ∈ ↑(s ×ˢ t)
b : α × α
x✝ : b ∈ ↑(s ×ˢ t)
⊢ (fun x => ((x.1, x.1), x.2, x.2)) a = (fun x => ((x.1, x.1), x.2, x.2)) b → a = b

Tactic:
simp only [Prod.mk.inj_iff, and_self_iff, and_imp]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a : α × α
x✝¹ : a ∈ ↑(s ×ˢ t)
b : α × α
x✝ : b ∈ ↑(s ×ˢ t)
⊢ a.1 = b.1 → a.2 = b.2 → a = b
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem _root_.Basis.coe_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    (v.toOrthonormalBasis hv : ι → E) = (v : ι → E) :=
  calc
    (v.toOrthonormalBasis hv : ι → E) = ((v.toOrthonormalBasis hv).toBasis : ι → E)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv) = ⇑(v.toOrthonormalBasis hv).toBasis

Tactic:
rw [OrthonormalBasis.coe_toBasis]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv) = ⇑(v.toOrthonormalBasis hv).toBasis

Tactic:
classical rw [OrthonormalBasis.coe_toBasis]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv).toBasis = ⇑v

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem exists_mem_multiset_dvd (hp : Prime p) {s : Multiset α} : p ∣ s.prod → ∃ a ∈ s, p ∣ a :=
  Multiset.induction_on s (fun h => (hp.not_dvd_one h).elim) fun a s ih h =>
    have : p ∣ a * s.prod

Proof state:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem top_himp : ⊤ ⇨ a = a :=
  eq_of_forall_le_iff fun b => by rw [le_himp_iff, inf_top_eq]

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a

Tactic:
rw [le_himp_iff, inf_top_eq]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_mul_X_pow (p : R⟦X⟧) (n d : ℕ) :
    coeff R (d + n) (p * X ^ n) = coeff R d p

Proof state:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff R (d, n).1) p * (coeff R (d, n).2) (X ^ n) = 0

Tactic:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Result:
no goals

Proof state:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff R b.1) p * (coeff R b.2) (X ^ n) = 0

Tactic:
rintro ⟨i, j⟩ h1 h2

Result:
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (coeff R (i, j).1) p * (coeff R (i, j).2) (X ^ n) = 0

Proof state:
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (coeff R (i, j).1) p * (coeff R (i, j).2) (X ^ n) = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Tactic:
rintro rfl

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).1 = d
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Tactic:
subst h1

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff R (d + n)) (p * X ^ n) = (coeff R d) p

Tactic:
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]

Result:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff R b.1) p * (coeff R b.2) (X ^ n) = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff R (d, n).1) p * (coeff R (d, n).2) (X ^ n) = 0

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Tactic:
rw [mem_antidiagonal, add_right_cancel_iff] at h1

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).1 = d
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Tactic:
rfl

Result:
no goals

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False

Tactic:
apply h2

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem finTwoProd_one (R : Type*) [Semiring R] : Basis.finTwoProd R 1 = (0, 1)

Proof state:
R : Type u_7
inst✝ : Semiring R
⊢ (Basis.finTwoProd R) 1 = (0, 1)

Tactic:
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem ConjClasses.card_carrier {G : Type*} [Group G] [Fintype G] (g : G)
    [Fintype (ConjClasses.mk g).carrier] [Fintype <| MulAction.stabilizer (ConjAct G) g] :
    Fintype.card (ConjClasses.mk g).carrier =
      Fintype.card G / Fintype.card (MulAction.stabilizer (ConjAct G) g)

Proof state:
case H
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
exact Fintype.card_pos_iff.mpr inferInstance

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier =
    Fintype.card (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card ↑(MulAction.orbit (ConjAct G) g)

Tactic:
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier =
    Fintype.card (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card ↑(MulAction.orbit (ConjAct G) g)

case H
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)