harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.of_mapCocone (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F}
    [∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G]
    [∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G]
    [ReflectsLimitsOfShape WalkingCospan G]
    [PreservesColimitsOfShape J G]
    [ReflectsColimitsOfShape J G]
    (H : IsVanKampenColimit (G.mapCocone c)) : IsVanKampenColimit c

Proof state:
case w.h
J : Type v'
inst✝⁷ : Category.{u', v'} J
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝⁴ : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst✝³ : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst✝² : ReflectsLimitsOfShape WalkingCospan G
inst✝¹ : PreservesColimitsOfShape J G
inst✝ : ReflectsColimitsOfShape J G
H : IsVanKampenColimit (G.mapCocone c)
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (Functor.const J).map (G.map f)).app j

Tactic:
simpa using G.congr_map (NatTrans.congr_app h j)

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem gronwallBound_continuous_ε (δ K x : ℝ) : Continuous fun ε => gronwallBound δ K ε x

Proof state:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => δ + ε * x

Tactic:
exact continuous_const.add (continuous_id.mul continuous_const)

Result:
no goals

Proof state:
δ K x : ℝ
⊢ Continuous fun ε => gronwallBound δ K ε x

Tactic:
by_cases hK : K = 0

Result:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x

case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x

Proof state:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x

Tactic:
simp only [gronwallBound_K0, hK]

Result:
case pos
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => δ + ε * x

Proof state:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)

Tactic:
exact continuous_const.add ((continuous_id.mul continuous_const).mul continuous_const)

Result:
no goals

Proof state:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x

Tactic:
simp only [gronwallBound_of_K_ne_0 hK]

Result:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem le_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
    [i₁ : Std.Asymm (· < · : α → α → Prop)]
    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
    {a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : a :: l₁ ≤ a :: l₂
⊢ l₁ ≤ l₂

Tactic:
rw [cons_le_cons_iff] at h

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : a < a ∨ a = a ∧ l₁ ≤ l₂
⊢ l₁ ≤ l₂

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : a < a ∨ a = a ∧ l₁ ≤ l₂
⊢ l₁ ≤ l₂

Tactic:
rcases h with h | ⟨_, h⟩

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : a < a
⊢ l₁ ≤ l₂

case inr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
left✝ : a = a
h : l₁ ≤ l₂
⊢ l₁ ≤ l₂

Proof state:
case inr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
left✝ : a = a
h : l₁ ≤ l₂
⊢ l₁ ≤ l₂

Tactic:
exact h

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : a < a
⊢ l₁ ≤ l₂

Tactic:
exact False.elim (i₀.irrefl _ h)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
lemma monic_X_add_C {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
    m.Monic (X i + C r)

Proof state:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.Monic (X i + C r)

Tactic:
apply monic_X.add_of_lt

Result:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Proof state:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Tactic:
simp [degree_C, degree_X, ← not_le, ← eq_zero_iff]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i + C r)

Tactic:
nontriviality R

Result:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.Monic (X i + C r)
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_sum (p : T[X]) (g : ℕ → T → R[X]) (x : S) :
    (p.sum g).eval₂ f x = p.sum fun n a => (g n a).eval₂ f x

Proof state:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
⊢ eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)

Tactic:
have A : ∀ y, eval₂ f x y = T y := fun y => rfl

Result:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)

Tactic:
let T : R[X] →+ S :=
  { toFun := eval₂ f x
    map_zero' := eval₂_zero _ _
    map_add' := fun p q => eval₂_add _ _ }

Result:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
⊢ eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)

Proof state:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ T (p.sum g) = p.sum fun n a => T (g n a)

Tactic:
rw [sum, map_sum, sum]

Result:
no goals

Proof state:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)

Tactic:
simp only [A]

Result:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ T (p.sum g) = p.sum fun n a => T (g n a)
-- Mathlib/Data/Num/Lemmas.lean
theorem div_zero (n : ZNum) : n / 0 = 0 :=
  show n.div 0 = 0 by cases n <;> rfl

Proof state:
n : ZNum
⊢ n.div 0 = 0

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem LipschitzWith.integrable_comp_iff_of_antilipschitz {K K'} {f : α → β} {g : β → γ}
    (hg : LipschitzWith K g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) :
    Integrable (g ∘ f) μ ↔ Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
K K' : ℝ≥0
f : α → β
g : β → γ
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ Integrable (g ∘ f) μ ↔ Integrable f μ

Tactic:
simp [← memLp_one_iff_integrable, hg.memLp_comp_iff_of_antilipschitz hg' g0]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma coheight_le_iff {a : α} {n : ℕ∞} :
    coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ p.head → p.length ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑p.length ≤ n

Tactic:
rw [coheight_eq, iSup₂_le_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_inv_hom (X : C) {Y Z : C} (f : Y ≅ Z) :
    X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem twoPow_and (x : BitVec w) (i : Nat) :
    (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ twoPow w i &&& x = if x.getLsbD i = true then twoPow w i else 0#w

Tactic:
rw [BitVec.and_comm, and_twoPow]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem bddAbove_insert [IsDirected α (· ≤ ·)] {s : Set α} {a : α} :
    BddAbove (insert a s) ↔ BddAbove s

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s : Set α
a : α
⊢ BddAbove (insert a s) ↔ BddAbove s

Tactic:
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem quotEquivOfEq_symm (h : I = J) :
    (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq h.symm

Proof state:
case h
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotEquivOfEq h).symm = quotEquivOfEq ⋯

Tactic:
ext

Result:
case h
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem frobenius_mk (x : ℕ × K) :
    (frobenius (PerfectClosure K p) p : PerfectClosure K p → PerfectClosure K p) (mk K p x) =
      mk _ _ (x.1, x.2 ^ p)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x ^ p = mk K p (x.1, x.2 ^ p)

Tactic:
exact mk_pow K p x p

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ (frobenius (PerfectClosure K p) p) (mk K p x) = mk K p (x.1, x.2 ^ p)

Tactic:
simp only [frobenius_def]

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x ^ p = mk K p (x.1, x.2 ^ p)
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
/-- An even Dirichlet character is an even function. -/
lemma Even.to_fun {χ : DirichletCharacter S m} (hχ : Even χ) : Function.Even χ :=
  fun _ ↦ by rw [← neg_one_mul, map_mul, hχ, one_mul]

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x✝ : ZMod m
⊢ χ (-x✝) = χ x✝

Tactic:
rw [← neg_one_mul, map_mul, hχ, one_mul]

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem fst_pred_mem_erase_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
    (m.1 - 1, m.2) ∈ b.erase m

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ (m.1 - 1, m.2) ∈ Finset.erase b m

Tactic:
rw [mem_right] at h

Result:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b
⊢ (m.1 - 1, m.2) ∈ Finset.erase b m

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b
⊢ (m.1 - 1, m.2) ≠ m

Tactic:
exact ne_of_apply_ne Prod.fst (pred_ne_self m.1)

Result:
no goals

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b
⊢ (m.1 - 1, m.2) ∈ Finset.erase b m

Tactic:
apply Finset.mem_erase_of_ne_of_mem _ h.2

Result:
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.1 - 1, m.2) ∈ b
⊢ (m.1 - 1, m.2) ≠ m
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.cos (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Adjunction.lean
lemma comparison_full [R.Full] {L : C ⥤ D} (adj : L ⊣ R) :
    (Monad.comparison adj).Full where
  map_surjective f := ⟨R.preimage f.f, by aesop_cat⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : R.Full
L : C ⥤ D
adj : L ⊣ R
X✝ Y✝ : D
f : (Monad.comparison adj).obj X✝ ⟶ (Monad.comparison adj).obj Y✝
⊢ (Monad.comparison adj).map (R.preimage f.f) = f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem boxProd_degree (x : α × β)
    [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] [Fintype ((G □ H).neighborSet x)] :
    (G □ H).degree x = G.degree x.1 + H.degree x.2

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
rw [degree, degree, degree, boxProd_neighborFinset, Finset.card_disjUnion]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
-- Mathlib/Order/WithBot.lean
lemma le_untop_iff (hy : y ≠ ⊤) : a ≤ untop y hy ↔ a ≤ y

Proof state:
case intro
α : Type u_1
a : α
inst✝ : LE α
y : α
hy : ↑y ≠ ⊤
⊢ a ≤ (↑y).untop hy ↔ ↑a ≤ ↑y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LE α
y : WithTop α
hy : y ≠ ⊤
⊢ a ≤ y.untop hy ↔ ↑a ≤ y

Tactic:
lift y to α using id hy

Result:
case intro
α : Type u_1
a : α
inst✝ : LE α
y : α
hy : ↑y ≠ ⊤
⊢ a ≤ (↑y).untop hy ↔ ↑a ≤ ↑y
-- Mathlib/NumberTheory/Dioph.lean
theorem sumsq_nonneg (x : α → ℕ) : ∀ l, 0 ≤ sumsq l x
  | [] => le_refl 0
  | p::ps => by
    rw [sumsq]
    exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ (sumsq (p :: ps)) x

Tactic:
rw [sumsq]

Result:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ (p * p + sumsq ps) x

Proof state:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ (p * p + sumsq ps) x

Tactic:
exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_preΨ (n : ℤ) : (W.map f).preΨ n = (W.preΨ n).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).preΨ n = Polynomial.map f (W.preΨ n)

Tactic:
simp only [preΨ, map_Ψ₂Sq, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_preNormEDS]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ preNormEDS ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n =
    preNormEDS ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ preNormEDS ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n =
    preNormEDS ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n

Tactic:
map_simp

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_map (f : α →₀ ℕ) (g : α → β) :
    f.toMultiset.map g = toMultiset (f.mapDomain g)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))

Tactic:
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
  toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
  (Multiset.mapAddMonoidHom g).map_nsmul]

Result:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ n • (Multiset.mapAddMonoidHom g) {a} + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)

Proof state:
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)

Tactic:
refine f.induction ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset 0) = toMultiset (mapDomain g 0)

case refine_2
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
          Multiset.map g (toMultiset (single a b + f)) = toMultiset (mapDomain g (single a b + f))

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
          Multiset.map g (toMultiset (single a b + f)) = toMultiset (mapDomain g (single a b + f))

Tactic:
intro a n f _ _ ih

Result:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ Multiset.map g (toMultiset (single a n + f)) = toMultiset (mapDomain g (single a n + f))

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ n • (Multiset.mapAddMonoidHom g) {a} + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset 0) = toMultiset (mapDomain g 0)

Tactic:
rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem cons_map_snd_darts {u v : V} (p : G.Walk u v) : (u :: p.darts.map (·.snd)) = p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: List.map (fun x => x.toProd.2) p.darts = p.support

Tactic:
induction p <;> simp! [*]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem sub : @Primrec' 2 fun v => v.head - v.tail.head

Proof state:
⊢ Primrec' fun v => (fun a b => b - a) v.head v.tail.head

Tactic:
refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_

Result:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head = (fun a b => b - a) v.head v.tail.head

Proof state:
⊢ Primrec' fun v => v.head - v.tail.head

Tactic:
have : @Primrec' 2 fun v ↦ (fun a b ↦ b - a) v.head v.tail.head := by
  refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
  simp; induction v.head <;> simp [*, Nat.sub_add_eq]

Result:
this : Primrec' fun v => (fun a b => b - a) v.head v.tail.head
⊢ Primrec' fun v => v.head - v.tail.head

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head = (fun a b => b - a) v.head v.tail.head

Tactic:
simp

Result:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => IH - 1) v.head = v.tail.head - v.head

Proof state:
this : Primrec' fun v => (fun a b => b - a) v.head v.tail.head
⊢ Primrec' fun v => v.head - v.tail.head

Tactic:
simpa using comp₂ (fun a b => b - a) this (tail head) head

Result:
no goals

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => IH - 1) v.head = v.tail.head - v.head

Tactic:
induction v.head <;> simp [*, Nat.sub_add_eq]

Result:
no goals
-- Mathlib/Topology/Bornology/Constructions.lean
theorem boundedSpace_induced_iff {α β : Type*} [Bornology β] {f : α → β} :
    @BoundedSpace α (Bornology.induced f) ↔ IsBounded (range f)

Proof state:
α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)

Tactic:
rw [← @isBounded_univ _ (Bornology.induced f), isBounded_induced, image_univ]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem liftOn_mk' {p : Sort u} (f : M → S → p) (H) (a : M) (b : S) :
    liftOn ((monoidOf S).mk' a b) f H = f a b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ ((monoidOf S).mk' a b).liftOn f H = f a b

Tactic:
rw [← mk_eq_monoidOf_mk', liftOn_mk]

Result:
no goals