harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card [FiniteDimensional L W]
    {t : Finset W} (h : finrank L W + 1 < t.card) :
    ∃ f : W → L, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Proof state:
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
obtain ⟨f, sum, total, nonzero⟩ :=
  Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card h

Result:
case intro.intro.intro
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
f : W → L
sum : ∑ e ∈ t, f e • e = 0
total : ∑ e ∈ t, f e = 0
nonzero : ∃ x ∈ t, f x ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Proof state:
case intro.intro.intro
L : Type u_1
inst✝³ : LinearOrderedField L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
f : W → L
sum : ∑ e ∈ t, f e • e = 0
total : ∑ e ∈ t, f e = 0
nonzero : ∃ x ∈ t, f x ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Connected.ofBoxProdRight (h : (G □ H).Connected) : H.Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ H.Connected

Tactic:
haveI := (nonempty_prod.1 h.nonempty).1

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ H.Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ H.Connected

Tactic:
haveI := (nonempty_prod.1 h.nonempty).2

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ H.Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ H.Connected

Tactic:
exact ⟨h.preconnected.ofBoxProdRight⟩

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem «exists» {p : ℚ → Prop} : (∃ r, p r) ↔ ∃ a b : ℤ, p (a / b) :=
  ⟨fun ⟨r, hr⟩ => ⟨r.num, r.den, by convert hr; convert num_div_den r⟩, fun ⟨_, _, h⟩ => ⟨_, h⟩⟩

Proof state:
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ p (↑r.num / ↑↑r.den)

Tactic:
convert hr

Result:
case h.e'_1
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ ↑r.num / ↑↑r.den = r

Proof state:
case h.e'_1
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ ↑r.num / ↑↑r.den = r

Tactic:
convert num_div_den r

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem id : AntilipschitzWith 1 (id : α → α) := fun x y => by
  simp only [ENNReal.coe_one, one_mul, id, le_refl]

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist x y ≤ ↑1 * edist (id x) (id y)

Tactic:
simp only [ENNReal.coe_one, one_mul, id, le_refl]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem coprod_bot (l : Filter α) : l.coprod (⊥ : Filter β) = comap Prod.fst l

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
⊢ l.coprod ⊥ = comap Prod.fst l

Tactic:
simp [Filter.coprod]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_neg_neg (x y : E) : ⟪-x, -y⟫ = ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪-x, -y⟫_𝕜 = ⟪x, y⟫_𝕜

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem card_insertNone (s : Finset α) : s.insertNone.card = s.card + 1

Proof state:
α : Type u_1
s : Finset α
⊢ #(insertNone s) = #s + 1

Tactic:
simp [insertNone]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem prec' {n f g h} (hf : @Primrec' n f) (hg : @Primrec' n g) (hh : @Primrec' (n + 2) h) :
    @Primrec' n fun v => (f v).rec (g v) fun y IH : ℕ => h (y ::ᵥ IH ::ᵥ v)

Proof state:
n : ℕ
f g : List.Vector ℕ n → ℕ
h : List.Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)

Tactic:
simpa using comp' (prec hg hh) (hf.cons idv)

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
    I • (⨆ i, t i)= ⨆ i, I • t i :=
  toAddSubmonoid_injective <| by
    simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
I : Submodule R A
t : ι → Submodule R M
⊢ (I • ⨆ i, t i).toAddSubmonoid = (⨆ i, I • t i).toAddSubmonoid

Tactic:
simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem split_by_characteristic_domain [IsDomain R] (h_pos : ∀ p : ℕ, Nat.Prime p → CharP R p → P)
    (h_equal : Algebra ℚ R → P) (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P

Tactic:
intro p p_pos p_char

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P

Tactic:
have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_prime : Nat.Prime p
⊢ P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_prime : Nat.Prime p
⊢ P

Tactic:
exact h_pos p p_prime p_char

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
refine split_by_characteristic R ?_ h_equal h_mixed

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P
-- Mathlib/Data/Real/ConjExponents.lean
protected lemma Real.IsConjExponent.toNNReal {p q : ℝ} (hpq : p.IsConjExponent q) :
    p.toNNReal.IsConjExponent q.toNNReal where
  one_lt

Proof state:
p q : ℝ
hpq : p.IsConjExponent q
⊢ 1 < p.toNNReal

Tactic:
simpa using hpq.one_lt

Result:
no goals

Proof state:
p q : ℝ
hpq : p.IsConjExponent q
⊢ p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1

Tactic:
rw [← toNNReal_inv, ← toNNReal_inv, ← toNNReal_add hpq.inv_nonneg
hpq.symm.inv_nonneg, hpq.inv_add_inv_conj, toNNReal_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
then `F` preserves colimits for `K`. -/
lemma preservesColimit_of_reflects_of_preserves
    [PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] :
    PreservesColimit K F :=
  ⟨fun {c} h => ⟨by
    apply isColimitOfReflects G
    apply isColimitOfPreserves (F ⋙ G) h⟩⟩

Proof state:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))

Tactic:
apply isColimitOfPreserves (F ⋙ G) h

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
apply isColimitOfReflects G

Result:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : Array α) (init : β) :
    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
l : Array α
init : β
⊢ foldr f init (filter p l) = foldr (fun x y => if p x = true then f x y else y) init l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
init : β
l : List α
⊢ foldr f init (filter p { toList := l }) = foldr (fun x y => if p x = true then f x y else y) init { toList := l }

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
init : β
l : List α
⊢ foldr f init (List.filter p l).toArray = foldr (fun x y => if p x = true then f x y else y) init { toList := l }

Tactic:
simp [List.foldr_filter]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
init : β
l : List α
⊢ foldr f init (filter p { toList := l }) = foldr (fun x y => if p x = true then f x y else y) init { toList := l }

Tactic:
rw [List.filter_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
init : β
l : List α
⊢ foldr f init (List.filter p l).toArray = foldr (fun x y => if p x = true then f x y else y) init { toList := l }
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum_ground (M : Matroid α) (N : Matroid β) :
    (M.sum N).E = (.inl '' M.E) ∪ (.inr '' N.E)

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
⊢ (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E

Tactic:
simp [Matroid.sum, Set.ext_iff, mapEquiv, mapEmbedding, Equiv.ulift, Equiv.sumEquivSigmaBool]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
lemma IsHomeomorph.sigmaMap {ι κ : Type*} {X : ι → Type*} {Y : κ → Type*}
    [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : ι → κ}
    (hf : Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ i, IsHomeomorph (g i)) :
    IsHomeomorph (Sigma.map f g)

Proof state:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
⊢ IsHomeomorph (Sigma.map f g)

Tactic:
simp_rw [isHomeomorph_iff_isEmbedding_surjective,] at hg ⊢

Result:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)
⊢ IsEmbedding (Sigma.map f g) ∧ Surjective (Sigma.map f g)

Proof state:
ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsEmbedding (g i) ∧ Surjective (g i)
⊢ IsEmbedding (Sigma.map f g) ∧ Surjective (Sigma.map f g)

Tactic:
exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩

Result:
no goals
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem mulIndicator_biUnion_finset_eventuallyEq {ι} [One β] (s : ι → Set α) (f : α → β) (a : α) :
    (fun n : Finset ι => mulIndicator (⋃ i ∈ n, s i) f a) =ᶠ[atTop]
      fun _ ↦ mulIndicator (iUnion s) f a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x => (iUnion s).mulIndicator f a

Tactic:
rw [iUnion_eq_iUnion_finset s]

Result:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ t, ⋃ i ∈ t, s i).mulIndicator f a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ t, ⋃ i ∈ t, s i).mulIndicator f a

Tactic:
apply Monotone.mulIndicator_eventuallyEq_iUnion

Result:
case hs
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun i => ⋃ i_1 ∈ i, s i_1

Proof state:
case hs
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun i => ⋃ i_1 ∈ i, s i_1

Tactic:
exact fun _ _ ↦ biUnion_subset_biUnion_left

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem vanishingIdeal_anti_mono_iff {s t : Set (PrimeSpectrum R)} (ht : IsClosed t) :
    s ⊆ t ↔ vanishingIdeal t ≤ vanishingIdeal s :=
  ⟨vanishingIdeal_anti_mono, fun h => by
    rw [← ht.closure_subset_iff, ← ht.closure_eq]
    convert ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t

Tactic:
convert ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t

Tactic:
rw [← ht.closure_subset_iff, ← ht.closure_eq]

Result:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_η_fst : (η (prod' F G)).1 = η F

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).1 = η F

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).1 = η F

Tactic:
change F.map (𝟙 _)  ≫ _ = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ F.map (𝟙 ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ F.map (𝟙 ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F

Tactic:
rw [Functor.map_id, Category.id_comp]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).1 = η F
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositions_iff {X Y : C} (f : X ⟶ Y) :
    transfiniteCompositions.{w} W f ↔
      ∃ (J : Type w) (_ : LinearOrder J) (_ : SuccOrder J) (_ : OrderBot J)
        (_ : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ transfiniteCompositions.{w, v, u} W f ↔ ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

Tactic:
simp only [transfiniteCompositions, iSup_iff]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem _root_.ZMod.card_units_eq_totient (n : ℕ) [NeZero n] [Fintype (ZMod n)ˣ] :
    Fintype.card (ZMod n)ˣ = φ n :=
  calc
    Fintype.card (ZMod n)ˣ = Fintype.card { x : ZMod n // x.val.Coprime n } :=
      Fintype.card_congr ZMod.unitsEquivCoprime
    _ = φ n

Proof state:
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if a.val.Coprime (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if (↑i).Coprime (m + 1) then 1 else 0

Tactic:
rfl

Result:
no goals

Proof state:
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // x.val.Coprime (m + 1) } = φ (m + 1)

Tactic:
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
  Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]

Result:
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if a.val.Coprime (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if (↑i).Coprime (m + 1) then 1 else 0

Proof state:
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // x.val.Coprime n } = φ n

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out

Result:
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // x.val.Coprime (m + 1) } = φ (m + 1)
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc (attr := simp)]
lemma pullbackAwayιIso_inv_snd :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.snd _ _ =
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _))))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') =
    Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯))

Tactic:
rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast?_zipIdx (l : List α) (k : Nat) :
    (zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1)

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ Option.map (fun a => (a, k + (l.length - 1))) l[l.length - 1]? =
    Option.map (fun a => (a, k + l.length - 1)) l[l.length - 1]?

Tactic:
cases l <;> simp

Result:
case cons
α : Type u_1
k : Nat
head✝ : α
tail✝ : List α
⊢ k + tail✝.length = k + (tail✝.length + 1) - 1

Proof state:
case cons
α : Type u_1
k : Nat
head✝ : α
tail✝ : List α
⊢ k + tail✝.length = k + (tail✝.length + 1) - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ (l.zipIdx k).getLast? = Option.map (fun a => (a, k + l.length - 1)) l.getLast?

Tactic:
simp [getLast?_eq_getElem?]

Result:
α : Type u_1
l : List α
k : Nat
⊢ Option.map (fun a => (a, k + (l.length - 1))) l[l.length - 1]? =
    Option.map (fun a => (a, k + l.length - 1)) l[l.length - 1]?
-- Mathlib/Computability/Tape.lean
theorem Tape.mk'_nth_nat {Γ} [Inhabited Γ] (L R : ListBlank Γ) (n : ℕ) :
    (Tape.mk' L R).nth n = R.nth n

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
n : ℕ
⊢ (mk' L R).nth ↑n = R.nth n

Tactic:
rw [← Tape.right₀_nth, Tape.mk'_right₀]

Result:
no goals
-- Mathlib/Algebra/Ring/Centralizer.lean
theorem neg_mem_centralizer [Mul M] [HasDistribNeg M] (ha : a ∈ centralizer S) :
    -a ∈ centralizer S := fun c hc => by rw [mul_neg, ha c hc, neg_mul]

Proof state:
M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * -a = -a * c

Tactic:
rw [mul_neg, ha c hc, neg_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
@[simp]
lemma fiberPullbackEquiv_symm_snd_apply {X A B : C} {f : A ⟶ X} {g : B ⟶ X}
    (a : F.obj A) (b : F.obj B) (h : F.map f a = F.map g b) :
    F.map (pullback.snd f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫
        (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.snd f g))
      ⟨(a, b), h⟩ =
    b

Tactic:
erw [PreservesPullback.iso_inv_snd, Types.pullbackIsoPullback_inv_snd]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.snd f g)
      ((PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv
        ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ⟨(a, b), h⟩)) =
    b

Tactic:
change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫
  (F ⋙ FintypeCat.incl).map (pullback.snd f g)) _ = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫
        (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.snd f g))
      ⟨(a, b), h⟩ =
    b

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.snd f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

Tactic:
simp [fiberPullbackEquiv]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.snd f g)
      ((PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv
        ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ⟨(a, b), h⟩)) =
    b
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_of_re_neg_of_im_neg {x : ℂ} (hx_re : x.re < 0) (hx_im : x.im < 0) :
    arg x = Real.arcsin ((-x).im / ‖x‖) - π

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) - π

Tactic:
simp only [arg, hx_re.not_le, hx_im.not_le, if_false]

Result:
no goals