harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Defs.lean
theorem mod_coe (m k : ℕ+) :
    (mod m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ))

Proof state:
case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = ↑k

Tactic:
rfl

Result:
no goals

Proof state:
case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = if 0 = 0 then ↑k else 0

Tactic:
rw [if_pos rfl]

Result:
case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = ↑k

Proof state:
m k : ℕ+
⊢ ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl

Result:
no goals

Proof state:
m k : ℕ+
⊢ ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
dsimp [mod, modDiv]

Result:
m k : ℕ+
⊢ ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Proof state:
case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = n + 1

Tactic:
rfl

Result:
no goals

Proof state:
case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = if n + 1 = 0 then ↑k else n + 1

Tactic:
rw [if_neg n.succ_ne_zero]

Result:
case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = n + 1
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem uncurry_id_eq_ev : uncurry (𝟙 (A ⟶[C] X)) = (ihom.ev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ uncurry (𝟙 ((ihom A).obj X)) = (ihom.ev A).app X

Tactic:
simp [uncurry_eq]

Result:
no goals
-- Mathlib/Tactic/PNatToNat.lean
@[pnat_to_nat_coe]
lemma sub_coe (a b : PNat) : ((a - b : PNat) : Nat) = a.val - 1 - b.val + 1

Proof state:
case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(⟨val✝¹, property✝¹⟩ - ⟨val✝, property✝⟩) = ↑⟨val✝¹, property✝¹⟩ - 1 - ↑⟨val✝, property✝⟩ + 1

Tactic:
simp only [PNat.mk_coe, _root_.PNat.sub_coe, ← _root_.PNat.coe_lt_coe]

Result:
case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ (if val✝ < val✝¹ then val✝¹ - val✝ else 1) = val✝¹ - 1 - val✝ + 1

Proof state:
case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ (if val✝ < val✝¹ then val✝¹ - val✝ else 1) = val✝¹ - 1 - val✝ + 1

Tactic:
split_ifs <;> omega

Result:
no goals

Proof state:
case mk
b : ℕ+
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(⟨val✝, property✝⟩ - b) = ↑⟨val✝, property✝⟩ - 1 - ↑b + 1

Tactic:
cases b

Result:
case mk.mk
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(⟨val✝¹, property✝¹⟩ - ⟨val✝, property✝⟩) = ↑⟨val✝¹, property✝¹⟩ - 1 - ↑⟨val✝, property✝⟩ + 1

Proof state:
a b : ℕ+
⊢ ↑(a - b) = ↑a - 1 - ↑b + 1

Tactic:
cases a

Result:
case mk
b : ℕ+
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(⟨val✝, property✝⟩ - b) = ↑⟨val✝, property✝⟩ - 1 - ↑b + 1
-- Mathlib/Data/Nat/GCD/Basic.lean
lemma add_coprime_iff_left (h : c ∣ b) : Coprime (a + b) c ↔ Coprime a c

Proof state:
a b c : ℕ
h : c ∣ b
⊢ (a + b).Coprime c ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c

Proof state:
case intro
a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem closure_image_mem_nhds {s : Set α} {a : α} (di : IsDenseInducing i) (hs : s ∈ 𝓝 a) :
    closure (i '' s) ∈ 𝓝 (i a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure (i '' s) ∈ 𝓝 (i a)

Tactic:
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ closure (i '' s) ∈ 𝓝 (i a)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ U ⊆ closure (i '' s)

Tactic:
calc
  U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
  _ ⊆ closure (i '' s) := closure_mono (image_subset i sub)

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ closure (i '' s) ∈ 𝓝 (i a)

Tactic:
refine mem_of_superset (hUo.mem_nhds haU) ?_

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ U ⊆ closure (i '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ closure (i '' s) ∈ 𝓝 (i a)

Tactic:
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure (i '' s) ∈ 𝓝 (i a)
-- Mathlib/Data/Real/EReal.lean
lemma inv_nonneg_of_nonneg {a : EReal} (h : 0 ≤ a) : 0 ≤ a⁻¹

Proof state:
case h_real
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a

Tactic:
exact EReal.coe_nonneg.1 h

Result:
no goals

Proof state:
a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
cases a with
| h_bot | h_top => simp
| h_real a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

Result:
no goals

Proof state:
case h_top
h : 0 ≤ ⊤
⊢ 0 ≤ ⊤⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h_real
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ (↑a)⁻¹

Tactic:
rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]

Result:
case h_real
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a
-- Mathlib/Data/Nat/PrimeFin.lean
lemma primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n

Proof state:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0

Tactic:
exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩

Result:
no goals

Proof state:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors

Tactic:
simp only [subset_iff, mem_primeFactors, and_imp]

Result:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0
-- Mathlib/Topology/Instances/Int.lean
theorem pairwise_one_le_dist : Pairwise fun m n : ℤ => 1 ≤ dist m n

Proof state:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|

Tactic:
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Result:
no goals

Proof state:
⊢ Pairwise fun m n => 1 ≤ dist m n

Tactic:
intro m n hne

Result:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n

Proof state:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n

Tactic:
rw [dist_eq]

Result:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|

Proof state:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|

Tactic:
norm_cast

Result:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem Iio_mem_nhds (h : γ₁ < γ₂) : Iio γ₂ ∈ 𝓝 γ₁

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁

Tactic:
rcases eq_or_ne γ₁ 0 with (rfl | h₀) <;> simp [*, h.ne', Iio_mem_nhds_zero]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
a prime if `p ≠ 2`. -/
lemma prime_norm_toInteger_sub_one_of_prime_ne_two [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
    Prime (Algebra.norm ℤ (hζ.toInteger - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ↑↑p

Tactic:
exact Nat.prime_iff_prime_int.1 hp.out

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
rw [this]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ↑↑p

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
have := hζ.norm_toInteger_sub_one_of_prime_ne_two hodd

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem smul_iff [Monoid R] [StarMul R] [AddMonoid A] [StarAddMonoid A]
    [MulAction R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) (hu : IsUnit r) {x : A} :
    IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hrx : IsSelfAdjoint (↑r • x)
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
exact hr.inv.smul hrx

Result:
no goals

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
replace hr : IsSelfAdjoint r := Units.ext hr.star_eq

Result:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hrx : IsSelfAdjoint (↑r • x)
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint x

Tactic:
rw [← inv_smul_smul r x]

Result:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
refine ⟨fun hrx ↦ ?_, .smul hr⟩

Result:
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
hrx : IsSelfAdjoint (r • x)
⊢ IsSelfAdjoint x

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
hrx : IsSelfAdjoint (r • x)
⊢ IsSelfAdjoint x

Tactic:
lift r to Rˣ using hu

Result:
case intro
R : Type u_1
A : Type u_2
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint x
-- Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
@[reassoc (attr := simp)]
lemma ι_mapTrifunctorMapMap {X₁ Y₁ : GradedObject I₁ C₁} (f₁ : X₁ ⟶ Y₁)
    {X₂ Y₂ : GradedObject I₂ C₂} (f₂ : X₂ ⟶ Y₂)
    {X₃ Y₃ : GradedObject I₃ C₃} (f₃ : X₃ ⟶ Y₃)
    [HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p]
    [HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃) p]
    (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : p ⟨i₁, i₂, i₃⟩ = j) :
  ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p f₁ f₂ f₃ j =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
      ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_12, u_2} C₂
inst✝³ : Category.{u_13, u_3} C₃
inst✝² : Category.{u_14, u_4} C₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
      (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h

Tactic:
rw [assoc, assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
    (l.insert a).all f = (f a && l.all f)

Proof state:
α : Type u_1
f : α → Bool
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l).all f = (f a && l.all f)

Tactic:
simp [all_eq]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
private lemma iter_fp_bound (n k : ℕ) :
    let iter_next (n guess : ℕ) := (guess + n / guess) / 2;
    sqrt.iter n k ≤ iter_next n (sqrt.iter n k)

Proof state:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)

Tactic:
unfold sqrt.iter

Result:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Proof state:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
if h : (k + n / k) / 2 < k then
  simpa [if_pos h] using iter_fp_bound _ _
else
  simpa [if_neg h] using Nat.le_of_not_lt h

Result:
no goals

Proof state:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
simpa [if_pos h] using iter_fp_bound _ _

Result:
no goals

Proof state:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
simpa [if_neg h] using Nat.le_of_not_lt h

Result:
no goals

Proof state:
n k : ℕ
⊢ let iter_next := fun n guess => (guess + n / guess) / 2;
  sqrt.iter n k ≤ iter_next n (sqrt.iter n k)

Tactic:
intro iter_next

Result:
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_ratCast_iff {q : ℚ} :
    Irrational (√q) ↔ ¬IsSquare q ∧ 0 ≤ q

Proof state:
case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
rw [sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 hq.le)]

Result:
case inr
q : ℚ
hq : q < 0
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q

Proof state:
q : ℚ
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
obtain hq | hq := le_or_lt 0 q

Result:
case inl
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Proof state:
case inl
q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
simp_rw [irrational_sqrt_ratCast_iff_of_nonneg hq, and_iff_left hq]

Result:
no goals

Proof state:
case inr
q : ℚ
hq : q < 0
⊢ Irrational 0 ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
    (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) :
    HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e

Proof state:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g q s e
w✝ : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w✝
⊢ HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e

Tactic:
rcases hg with ⟨_, hg⟩

Result:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w✝¹ : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w✝¹
w✝ : ℝ≥0∞
hg : HasFPowerSeriesWithinOnBall g q s e w✝
⊢ HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e

Proof state:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w✝¹ : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w✝¹
w✝ : ℝ≥0∞
hg : HasFPowerSeriesWithinOnBall g q s e w✝
⊢ HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e

Tactic:
exact ⟨_, hf.prod hg⟩

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinAt f p s e
hg : HasFPowerSeriesWithinAt g q s e
⊢ HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e

Tactic:
rcases hf with ⟨_, hf⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g q s e
w✝ : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w✝
⊢ HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e
-- Mathlib/Data/Rel.lean
theorem image_preimage_subset_inter_codom (s : Set β) : s ∩ r.codom ⊆ r.image (r.preimage s)

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
⊢ s ∩ r.inv.dom ⊆ r.inv.preimage (r.preimage s)

Tactic:
apply inter_dom_subset_preimage_image

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
⊢ s ∩ r.codom ⊆ r.image (r.preimage s)

Tactic:
rw [← dom_inv, ← preimage_inv]

Result:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
⊢ s ∩ r.inv.dom ⊆ r.inv.preimage (r.preimage s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_succ (s n step) :
    range' s (n + 1) step = (#v[s] ++ range' (s + step) n step).cast (by omega)

Proof state:
s n step : Nat
⊢ 1 + n = n + 1

Tactic:
omega

Result:
no goals

Proof state:
s n step : Nat
⊢ (range' s (n + 1) step).toArray =
    (Vector.cast ⋯ ({ toArray := #[s], size_toArray := ⋯ } ++ range' (s + step) n step)).toArray

Tactic:
simp [Array.range'_succ]

Result:
no goals

Proof state:
s n step : Nat
⊢ range' s (n + 1) step = Vector.cast ⋯ ({ toArray := #[s], size_toArray := ⋯ } ++ range' (s + step) n step)

Tactic:
rw [← toArray_inj]

Result:
s n step : Nat
⊢ (range' s (n + 1) step).toArray =
    (Vector.cast ⋯ ({ toArray := #[s], size_toArray := ⋯ } ++ range' (s + step) n step)).toArray
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
  | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
  | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
  | _+1, _+1 => by
    rw [Nat.succ_sub_succ, Nat.succ_min_succ, Nat.succ_sub (Nat.sub_le ..)]
    exact congrArg succ <| Nat.sub_sub_eq_min ..

Proof state:
x✝ : Nat
⊢ x✝ - (x✝ - 0) = min x✝ 0

Tactic:
rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]

Result:
no goals

Proof state:
x✝ : Nat
⊢ 0 - (0 - x✝) = min 0 x✝

Tactic:
rw [Nat.zero_sub, Nat.zero_min]

Result:
no goals

Proof state:
n✝¹ n✝ : Nat
⊢ n✝¹ + 1 - (n✝¹ + 1 - (n✝ + 1)) = min (n✝¹ + 1) (n✝ + 1)

Tactic:
rw [Nat.succ_sub_succ, Nat.succ_min_succ, Nat.succ_sub (Nat.sub_le ..)]

Result:
n✝¹ n✝ : Nat
⊢ (n✝¹ - (n✝¹ - n✝)).succ = (min n✝¹ n✝).succ

Proof state:
n✝¹ n✝ : Nat
⊢ (n✝¹ - (n✝¹ - n✝)).succ = (min n✝¹ n✝).succ

Tactic:
exact congrArg succ <| Nat.sub_sub_eq_min ..

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : k ∉ m) (h' : (f (m.get? k)).isNone) : (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : ¬k ∈ m
h' : (f (m.get? k)).isNone = true
⊢ (m.alter k f).size = m.size

Tactic:
rw [mem_iff_contains, Bool.not_eq_true] at h

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.contains k = false
h' : (f (m.get? k)).isNone = true
⊢ (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.contains k = false
h' : (f (m.get? k)).isNone = true
⊢ (m.alter k f).size = m.size

Tactic:
exact Raw₀.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h'

Result:
no goals