harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n) :
    s.circumcenter =
      (univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
        (circumcenterWeightsWithCircumcenter n)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex

Tactic:
refine affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) rfl ?_

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ ∀ i2 ∈ univ, i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ ∀ i2 ∈ univ, i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0

Tactic:
rintro ⟨i⟩ _ hn <;> tauto

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)

Tactic:
symm

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ s.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)

Tactic:
rw [← pointsWithCircumcenter_eq_circumcenter]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_eq_arctan_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) :
    angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
-- Mathlib/Data/List/Intervals.lean
theorem inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = []

Proof state:
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l

Tactic:
simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]

Result:
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a

Proof state:
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
apply eq_nil_iff_forall_not_mem.2

Result:
n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l

Proof state:
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a

Tactic:
exfalso

Result:
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False

Proof state:
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False

Tactic:
exact not_lt_of_ge h₃ h₂

Result:
no goals

Proof state:
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a

Tactic:
intro _ h₂ h₃

Result:
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a

Proof state:
n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l

Tactic:
intro a

Result:
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_tmod_self (a : Int) : (-a).tmod a = 0

Proof state:
a : Int
⊢ (-a).tmod a = 0

Tactic:
rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]

Result:
a : Int
⊢ a ∣ a

Proof state:
a : Int
⊢ a ∣ a

Tactic:
exact Int.dvd_refl a

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma val_eq_ite_valMinAbs [NeZero n] (a : ZMod n) :
    (a.val : ℤ) = a.valMinAbs + if a.val ≤ n / 2 then 0 else n

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n) + ↑(if a.val ≤ n / 2 then 0 else n)

Tactic:
split_ifs <;> simp [add_zero, sub_add_cancel]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)

Tactic:
rw [valMinAbs_def_pos]

Result:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n) + ↑(if a.val ≤ n / 2 then 0 else n)
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_deleteEdges [DecidableEq V] [Fintype G.edgeSet] (s : Finset (Sym2 V))
    [Fintype (G.deleteEdges s).edgeSet] :
    (G.deleteEdges s).edgeFinset = G.edgeFinset \ s

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
⊢ (G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s

Tactic:
ext e

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
e : Sym2 V
⊢ e ∈ (G.deleteEdges ↑s).edgeFinset ↔ e ∈ G.edgeFinset \ s

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G.edgeSet
s : Finset (Sym2 V)
inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet
e : Sym2 V
⊢ e ∈ (G.deleteEdges ↑s).edgeFinset ↔ e ∈ G.edgeFinset \ s

Tactic:
simp [edgeSet_deleteEdges]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq :
    convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Proof state:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
cases s_succ_nth_eq : s.get? <| n + 1 with
| none =>
  rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
    convs'Aux_stable_step_of_terminated s_succ_nth_eq]
| some gp_succ_n =>
  induction n generalizing s gp_succ_n with
  | zero =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
      s.ge_stable zero_le_one s_succ_nth_eq
    have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
      squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
    simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
  | succ m IH =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
      s.ge_stable (m + 2).zero_le s_succ_nth_eq
    suffices
      gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
        convs'Aux (squashSeq s (m + 1)) (m + 2)
      by simpa only [convs'Aux, s_head_eq]
    have : (squashSeq s (m + 1)).head = some gp_head :=
      (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
    simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_neg_nat_eq_zero (n : ℕ) : Gamma (-n) = 0

Proof state:
n : ℕ
⊢ Gamma (-↑n) = 0

Tactic:
simpa only [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Complex.Gamma_ofReal,
  Complex.ofReal_eq_zero] using Complex.Gamma_neg_nat_eq_zero n

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem smul'_mk (r : R) (s : S) (m : M) : r • mk m s = mk (r • m) s

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : ↥S
m : M
⊢ mk (r • m) (1 * s) = mk (r • m) s

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : ↥S
m : M
⊢ r • mk m s = mk (r • m) s

Tactic:
erw [mk_smul_mk r m 1 s]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : ↥S
m : M
⊢ mk (r • m) (1 * s) = mk (r • m) s
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem one : padicValNat p 1 = 0

Proof state:
p : ℕ
⊢ padicValNat p 1 = 0

Tactic:
simp [padicValNat]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Finite.encard_eq_coe_toFinset_card (h : s.Finite) : s.encard = h.toFinset.card

Proof state:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ s.encard = ↑h.toFinset.card

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard = ↑h.toFinset.card

Tactic:
have := h.fintype

Result:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ s.encard = ↑h.toFinset.card
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_of_X_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) :
    W'.addY P Q * (P z * Q z) ^ 3 = -(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2

Proof state:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addY P Q * (P z * Q z) ^ 3 + -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
addZ_of_X_eq hP hQ hPz hQz hx]

Result:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Proof state:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addY P Q * (P z * Q z) ^ 3 = -(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2

Tactic:
linear_combination (norm := (rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
  addZ_of_X_eq hP hQ hPz hQz hx]; ring1)) -(P z * Q z) * negAddY_of_X_eq' hP hQ hx

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem nextCoeff_of_natDegree_pos (hp : 0 < p.natDegree) :
    nextCoeff p = p.coeff (p.natDegree - 1)

Proof state:
case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ ¬p.natDegree = 0

Tactic:
contrapose! hp

Result:
case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ p.natDegree ≤ 0

Proof state:
case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ p.natDegree ≤ 0

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ p.nextCoeff = p.coeff (p.natDegree - 1)

Tactic:
rw [nextCoeff, if_neg]

Result:
case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ ¬p.natDegree = 0
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem inv_iff {f : Perm α} : IsThreeCycle f⁻¹ ↔ IsThreeCycle f :=
  ⟨by
    rw [← inv_inv f]
    apply inv, inv⟩

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹.IsThreeCycle → f.IsThreeCycle

Tactic:
rw [← inv_inv f]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle

Tactic:
apply inv

Result:
no goals
-- Mathlib/Algebra/Star/Unitary.lean
theorem coe_div (U₁ U₂ : unitary R) : ↑(U₁ / U₂) = (U₁ / U₂ : R)

Proof state:
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U₁ U₂ : ↥(unitary R)
⊢ ↑(U₁ / U₂) = ↑U₁ / ↑U₂

Tactic:
simp only [div_eq_mul_inv, coe_inv, Submonoid.coe_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem _root_.mem_span_of_iInf_ker_le_ker [Finite ι] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜}
    (h : ⨅ i, ker (L i) ≤ ker K) : K ∈ span 𝕜 (range L)

Proof state:
case intro.h
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ (∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (p.liftQ K h ∘ₗ p.mkQ) x

Tactic:
convert LinearMap.congr_fun hK' (p.mkQ x)

Result:
case h.e'_2
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ (∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (∑ i : ι, c i • L' i) (p.mkQ x)
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma map_emptyOn (f : α → β) : (emptyOn α).map f (by simp) = emptyOn β

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn α).map f ⋯ = emptyOn β

Tactic:
simp [← ground_eq_empty_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ InjOn f (emptyOn α).E

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem noncommCoprod_apply' (comm) (mn : M × N) :
    (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Tactic:
rw [← comm, noncommCoprod_apply]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
/-- The term norms of any convergent series are bounded by a constant. -/
lemma exists_norm_le_of_cauchySeq (h : CauchySeq fun n ↦ ∑ k ∈ range n, f k) :
    ∃ C, ∀ n, ‖f n‖ ≤ C

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
⊢ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
refine ⟨b 0, fun n ↦ ?_⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
n : ℕ
⊢ ‖f n‖ ≤ b 0

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k
⊢ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
obtain ⟨b, ⟨_, key, _⟩⟩ := cauchySeq_iff_le_tendsto_0.mp h

Result:
case intro.intro.intro
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
⊢ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
n : ℕ
⊢ ‖f n‖ ≤ b 0

Tactic:
simpa only [dist_partial_sum'] using key n (n + 1) 0 (_root_.zero_le _) (_root_.zero_le _)

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem smul_fixedBy (g h : G) :
    h • fixedBy α g = fixedBy α (h * g * h⁻¹)

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
⊢ h • fixedBy α g = fixedBy α (h * g * h⁻¹)

Tactic:
ext a

Result:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)

Tactic:
simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
    (x ||| y) <<< n = (x <<< n) ||| (y <<< n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x ||| y) <<< n).getLsbD i = (x <<< n ||| y <<< n).getLsbD i

Tactic:
simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) || y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) || !decide (i < n) && y.getLsbD (i - n))

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) || y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) || !decide (i < n) && y.getLsbD (i - n))

Tactic:
by_cases h' : i < n <;> simp [h']

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ||| y) <<< n = x <<< n ||| y <<< n

Tactic:
ext i h

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x ||| y) <<< n).getLsbD i = (x <<< n ||| y <<< n).getLsbD i
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma freeLocus_congr {M'} [AddCommGroup M'] [Module R M'] (e : M ≃ₗ[R] M') :
    freeLocus R M = freeLocus R M'

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ freeLocus R M = freeLocus R M'

Tactic:
ext p

Result:
case h
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ p ∈ freeLocus R M ↔ p ∈ freeLocus R M'

Proof state:
case h
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ p ∈ freeLocus R M ↔ p ∈ freeLocus R M'

Tactic:
exact mem_freeLocus_of_isLocalization _ _ _
  (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_comm (a b : α) {i j : Nat} (v : Vector α n) {hi : i < n} {hj : j < n} (h : i ≠ j) :
    (v.set i a hi).set j b hj = (v.set j b hj).set i a hi

Proof state:
α : Type u_1
n : Nat
a b : α
i j : Nat
v : Vector α n
hi : i < n
hj : j < n
h : i ≠ j
⊢ (v.set i a hi).set j b hj = (v.set j b hj).set i a hi

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
a b : α
i j : Nat
hi : i < n
hj : j < n
h : i ≠ j
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a hi).set j b hj =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set j b hj).set i a hi

Proof state:
case mk
α : Type u_1
n : Nat
a b : α
i j : Nat
hi : i < n
hj : j < n
h : i ≠ j
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a hi).set j b hj =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set j b hj).set i a hi

Tactic:
simp [Array.set_comm, h]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.of_prod_one_sub
    (he : OrthogonalIdempotents e) (he' : ∏ i, (1 - e i) = 0) :
    CompleteOrthogonalIdempotents e where
  __ := he
  complete

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : ∏ i : I, (1 - e i) = 0
⊢ ∑ i : I, e i = 1

Tactic:
rwa [he.prod_one_sub, sub_eq_zero, eq_comm] at he'

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
/-- Values of an absolute value coincide on the image of `ℕ` in `R`
if and only if they coincide on the image of `ℤ` in `R`. -/
lemma eq_on_nat_iff_eq_on_int {f g : AbsoluteValue R S} :
    (∀ n : ℕ , f n = g n) ↔ ∀ n : ℤ , f n = g n

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n

Tactic:
refine ⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩

Result:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℤ
⊢ f ↑z = g ↑z

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℤ
⊢ f ↑z = g ↑z

Tactic:
obtain ⟨n , rfl | rfl⟩ := eq_nat_or_neg z <;> simp [h n]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.dist_left_right_div_two (h : s.IsDiameter p₁ p₂) :
    (dist p₁ p₂) / 2 = s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ / 2 = s.radius

Tactic:
simp [h.dist_left_right]

Result:
no goals
-- Mathlib/Data/List/SplitBy.lean
theorem chain'_of_mem_splitBy {r : α → α → Bool} {l : List α} (h : m ∈ l.splitBy r) :
    m.Chain' fun x y ↦ r x y

Proof state:
case cons
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ Chain' (fun x y => r x y = true) m

Tactic:
apply chain'_of_mem_splitByLoop _ _ h

Result:
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), b ∈ [].head? → r b a = true

α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ Chain' (fun y x => r x y = true) []

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ ∀ (b : α), b ∈ [].head? → r b a = true

Tactic:
rintro _ ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
a : α
l : List α
h : m ∈ splitBy r (a :: l)
⊢ Chain' (fun y x => r x y = true) []

Tactic:
exact chain'_nil

Result:
no goals

Proof state:
case nil
α : Type u_1
m : List α
r : α → α → Bool
h : m ∈ splitBy r []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
cases h

Result:
no goals