harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Limit.lean
theorem limitRecOn_succ_of_not_isMax (hb : ¬ IsMax b) :
    limitRecOn (Order.succ b) hm hs hl = hs b hb (limitRecOn b hm hs hl)

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
⊢ limitRecOn (Order.succ b) hm hs hl = hs b hb (limitRecOn b hm hs hl)

Tactic:
rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
⊢ hs b ?hb (prelimitRecOn b hs fun a ha IH => if h : IsMin a then hm a h else hl a ⋯ IH) =
    hs b hb (limitRecOn b hm hs hl)

case hb
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
⊢ ¬IsMax b

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
⊢ hs b ?hb (prelimitRecOn b hs fun a ha IH => if h : IsMin a then hm a h else hl a ⋯ IH) =
    hs b hb (limitRecOn b hm hs hl)

case hb
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
⊢ ¬IsMax b

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/MonoidalComp.lean
@[simp] lemma monoidalComp_refl {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    f ⊗≫ g = f ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ⊗≫ g = f ≫ g

Tactic:
simp [monoidalComp]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_algebraMap_mul (r : R) (b : CliffordAlgebra Q) :
    algebraMap _ _ r * b⌊d = algebraMap _ _ r * (b⌊d)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d =
    (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d

Tactic:
rw [← Algebra.smul_def, LinearMap.map_smul₂, Algebra.smul_def]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_lt_iff {a b : Ordinal} : a.toPGame < b.toPGame ↔ a < b :=
  ⟨by contrapose; rw [not_lt]; exact fun h => not_lt_of_le (toPGame_le h), toPGame_lt⟩

Proof state:
a b : Ordinal.{u_1}
⊢ b ≤ a → ¬a.toPGame < b.toPGame

Tactic:
exact fun h => not_lt_of_le (toPGame_le h)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬a.toPGame < b.toPGame

Tactic:
rw [not_lt]

Result:
a b : Ordinal.{u_1}
⊢ b ≤ a → ¬a.toPGame < b.toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ a.toPGame < b.toPGame → a < b

Tactic:
contrapose

Result:
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬a.toPGame < b.toPGame
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivativeFinsupp_derivative (p : R[X]) :
    derivativeFinsupp (derivative p) =
      (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ derivativeFinsupp (derivative p) = Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯

Tactic:
ext i : 1

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (derivativeFinsupp (derivative p)) i = (Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯) i

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (derivativeFinsupp (derivative p)) i = (Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯) i

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma exists_walk_of_edist_eq_coe {k : ℕ} (h : G.edist u v = k) :
    ∃ p : G.Walk u v, p.length = k :=
  have : G.edist u v ≠ ⊤

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤

Tactic:
exact ENat.coe_ne_top _

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ G.edist u v ≠ ⊤

Tactic:
rw [h]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P1_of_eq (he : x₁ ≈ x₃) (h₁ : P2 x₁ x₃ y₁) (h₃ : P2 x₁ x₃ y₃) (h3 : P3 x₁ x₂ y₂ y₃) :
    P1 x₁ x₂ x₃ y₁ y₂ y₃

Proof state:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
he : x₁ ≈ x₃
h₁ : P2 x₁ x₃ y₁
h₃ : P2 x₁ x₃ y₃
h3 : P3 x₁ x₂ y₂ y₃
⊢ ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₁ * y₃⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧

Tactic:
convert add_lt_add_left h3 ⟦x₁ * y₁⟧ using 1 <;> abel

Result:
no goals

Proof state:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
he : x₁ ≈ x₃
h₁ : P2 x₁ x₃ y₁
h₃ : P2 x₁ x₃ y₃
h3 : P3 x₁ x₂ y₂ y₃
⊢ P1 x₁ x₂ x₃ y₁ y₂ y₃

Tactic:
rw [P1, ← h₁ he, ← h₃ he, sub_lt_sub_iff]

Result:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
he : x₁ ≈ x₃
h₁ : P2 x₁ x₃ y₁
h₃ : P2 x₁ x₃ y₃
h3 : P3 x₁ x₂ y₂ y₃
⊢ ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₁ * y₃⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem sInf_isNormal (s : Set <| Subgroupoid C) (sn : ∀ S ∈ s, IsNormal S) : IsNormal (sInf s) :=
  { wide

Proof state:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
simp_rw [sInf, mem_iInter₂]

Result:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), ∀ i ∈ s, 𝟙 c ∈ i.arrows c c

Proof state:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), ∀ i ∈ s, 𝟙 c ∈ i.arrows c c

Tactic:
exact fun c S Ss => (sn S Ss).wide c

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, (∀ i ∈ s, γ ∈ i.arrows c c) → ∀ i ∈ s, Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d

Tactic:
exact fun p γ hγ S Ss => (sn S Ss).conj p (hγ S Ss)

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ (sInf s).arrows c c → Groupoid.inv p ≫ γ ≫ p ∈ (sInf s).arrows d d

Tactic:
simp_rw [sInf, mem_iInter₂]

Result:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, (∀ i ∈ s, γ ∈ i.arrows c c) → ∀ i ∈ s, Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c

Proof state:
a b c : Int
h : a + b = a + c
h₁ : b = c
⊢ b = c

Tactic:
exact h₁

Result:
no goals

Proof state:
a b c : Int
h : a + b = a + c
⊢ b = c

Tactic:
have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]

Result:
a b c : Int
h : a + b = a + c
h₁ : -a + (a + b) = -a + (a + c)
⊢ b = c

Proof state:
a b c : Int
h : a + b = a + c
⊢ -a + (a + b) = -a + (a + c)

Tactic:
rw [h]

Result:
no goals

Proof state:
a b c : Int
h : a + b = a + c
h₁ : -a + (a + b) = -a + (a + c)
⊢ b = c

Tactic:
simp [← Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁

Result:
a b c : Int
h : a + b = a + c
h₁ : b = c
⊢ b = c
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma ranObjObjIsoLimit_hom_π
    (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
    (L.ranObjObjIsoLimit F X).hom ≫ limit.π _ f =
    (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝² : Category.{u_5, u_3} H
inst✝¹ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
f : StructuredArrow X L
⊢ (L.ranObjObjIsoLimit F X).hom ≫ limit.π (StructuredArrow.proj X L ⋙ F) f =
    (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right

Tactic:
simp [ranObjObjIsoLimit, ran, ranCounit]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem strictMono_x : StrictMono (xn a1)
  | _, 0, h => absurd h <| Nat.not_lt_zero _
  | m, n + 1, h => by
    have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
        fun e => by rw [e]
    simp only [xn_succ, gt_iff_lt]
    refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)
    have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
    rwa [mul_one] at t

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 n * a + Pell.d a1 * yn a1 n

Tactic:
refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 n < xn a1 n * a

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ xn a1 m ≤ xn a1 n

Tactic:
rw [e]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ xn a1 m < xn a1 (n + 1)

Tactic:
have : xn a1 m ≤ xn a1 n :=
  Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
    fun e => by rw [e]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
t : xn a1 n * 1 < xn a1 n * a
⊢ xn a1 n < xn a1 n * a

Tactic:
rwa [mul_one] at t

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 n < xn a1 n * a

Tactic:
have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
t : xn a1 n * 1 < xn a1 n * a
⊢ xn a1 n < xn a1 n * a

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 (n + 1)

Tactic:
simp only [xn_succ, gt_iff_lt]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 n * a + Pell.d a1 * yn a1 n
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem snd_univ : ρ.snd univ = ρ univ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ ρ.snd univ = ρ univ

Tactic:
rw [snd_apply MeasurableSet.univ, preimage_univ]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 :=
  Polynomial.ext fun m => by
    rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero]
    split_ifs <;> rfl

Proof state:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (if m < n then 0 else 0) = 0

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (trunc n 0).coeff m = Polynomial.coeff 0 m

Tactic:
rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero]

Result:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (if m < n then 0 else 0) = 0
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_bot : (⊥ : Subgraph G).edgeSet = ∅ :=
  Set.ext <| Sym2.ind (by simp)

Proof state:
V : Type u
G : SimpleGraph V
⊢ ∀ (x y : V), s(x, y) ∈ ⊥.edgeSet ↔ s(x, y) ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow {n : ℕ} {a b : ℕ} (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod : n = a * b) :
    IsPrimitiveRoot (ζ ^ a) b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b

Tactic:
simp only [iff_def, ← pow_mul, h.pow_eq_one, true_and]

Result:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
⊢ IsPrimitiveRoot (ζ ^ a) b

Tactic:
subst n

Result:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l

Tactic:
exact Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_mul_pos_right hn) <| h.dvd_of_pow_eq_one _ hl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l

Tactic:
intro l hl

Result:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l
-- Mathlib/Topology/DiscreteQuotient.lean
theorem comap_mono {A B : DiscreteQuotient Y} (h : A ≤ B) : A.comap f ≤ B.comap f

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A B : DiscreteQuotient Y
h : A ≤ B
⊢ comap f A ≤ comap f B

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
  | (n : ℕ) => by
    rw [zpow_natCast]
    exact pow_mem hx n
  | -[n+1] => by
    rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K

Tactic:
exact inv_mem (pow_mem hx n.succ)

Result:
no goals

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K

Tactic:
exact pow_mem hx n

Result:
no goals

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ ↑n ∈ K

Tactic:
rw [zpow_natCast]

Result:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K

Tactic:
rw [zpow_negSucc]

Result:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem containsThenInsert_snd {k : α} {v : β k} : (m.containsThenInsert k v).2 = m.insert k v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (m.containsThenInsert k v).snd = m.insert k v

Tactic:
rw [containsThenInsert_eq_insertₘ, insert_eq_insertₘ]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
theorem mapsTo_coreflection_coroot :
    MapsTo (P.coreflection i) (range P.coroot) (range P.coroot)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ MapsTo (⇑(P.coreflection i)) (range ⇑P.coroot) (range ⇑P.coroot)

Tactic:
rintro - ⟨j, rfl⟩

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.coreflection i) (P.coroot j) ∈ range ⇑P.coroot

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.coreflection i) (P.coroot j) ∈ range ⇑P.coroot

Tactic:
exact P.coroot_reflection_perm i j ▸ mem_range_self (P.reflection_perm i j)

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
theorem simply_connected_iff_unique_homotopic (X : Type*) [TopologicalSpace X] :
    SimplyConnectedSpace X ↔
      Nonempty X ∧ ∀ x y : X, Nonempty (Unique (Path.Homotopic.Quotient x y))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
simp only [simply_connected_def, equiv_punit_iff_unique,
  FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ X →
    ((∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
      ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y)))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ X →
    ((∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
      ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y)))

Tactic:
intros

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a✝ : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a✝ : X
⊢ (∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

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

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean2_weighted {w₁ w₂ p₁ p₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂)
    (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hw : w₁ + w₂ = 1) : p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂ :=
  NNReal.geom_mean_le_arith_mean2_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ <|
    NNReal.coe_inj.1 <| by assumption

Proof state:
w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩) = ↑1

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
lemma preimage_val_sInter : A ↓∩ (⋂₀ S) = ⋂₀ { (A ↓∩ B) | B ∈ S }

Proof state:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂ a ∈ S, A ↓∩ a

Tactic:
simp_rw [sInter_eq_biInter, preimage_iInter]

Result:
no goals

Proof state:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
rw [← Set.image, sInter_image]

Result:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂ a ∈ S, A ↓∩ a
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_infinite (hs : s.Infinite) : count s = ∞

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑n ≤ count s

Tactic:
rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : ↑t ⊆ s
⊢ ↑t.card ≤ count s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : ↑t ⊆ s
⊢ ↑t.card = ∑ i ∈ t, 1

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : ↑t ⊆ s
⊢ ↑t.card ≤ count s

Tactic:
calc
  (t.card : ℝ≥0∞) = ∑ i ∈ t, 1 := by simp
  _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
  _ ≤ count (t : Set α) := le_count_apply
  _ ≤ count s := measure_mono ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
⊢ count s = ⊤

Tactic:
refine top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑n ≤ count s
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem volume_fundamentalDomain [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) :
    volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of b).det|

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| = ENNReal.ofReal |(Matrix.of ⇑b).transpose.det|

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det|

Tactic:
rw [measure_fundamentalDomain b volume (b₀ := Pi.basisFun ℝ ι), fundamentalDomain_pi_basisFun,
  volume_pi, Measure.pi_pi, Real.volume_Ico, sub_zero, ENNReal.ofReal_one, Finset.prod_const_one,
  mul_one, ← Matrix.det_transpose]

Result:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| = ENNReal.ofReal |(Matrix.of ⇑b).transpose.det|
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H

Tactic:
rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_single_one (α n) [Zero α] [One α] [DecidableEq n] [AddGroup n] :
    circulant (Pi.single 0 1 : n → α) = (1 : Matrix n n α)

Proof state:
case a
α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = 1 i j

Tactic:
simp [one_apply, Pi.single_apply, sub_eq_zero]

Result:
no goals

Proof state:
α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
⊢ circulant (Pi.single 0 1) = 1

Tactic:
ext i j

Result:
case a
α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = 1 i j
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma derivative_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁)
    (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
    derivative (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
      -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)) +
          (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
rw [addPolynomial_slope h₁ h₂ hxy]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ derivative (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -(((1 - 0) * (X - C x₂) + (X - C x₁) * (1 - 0)) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₁) * (X - C x₂) * (1 - 0)) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ derivative (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
derivative_simp

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -(((1 - 0) * (X - C x₂) + (X - C x₁) * (1 - 0)) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₁) * (X - C x₂) * (1 - 0)) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))