harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
lemma LFunctionTrivChar_isBigO_near_one_horizontal :
    (fun x : ℝ ↦ LFunctionTrivChar N (1 + x)) =O[𝓝[>] 0] fun x ↦ (1 : ℂ) / x

Proof state:
case h.e'_3
N : ℕ
inst✝ : NeZero N
⊢ (fun w => w * LFunctionTrivChar N (1 + w)) = (fun s => (s - 1) * LFunctionTrivChar N s) ∘ fun w => 1 + w

Tactic:
simp only [Function.comp_def, add_sub_cancel_left]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
this : (fun w => LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x
⊢ (fun x => LFunctionTrivChar N (1 + ↑x)) =O[𝓝[>] 0] fun x => 1 / ↑x

Tactic:
exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
H : Tendsto (fun w => w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))
⊢ (fun w => LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x

Tactic:
exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun w => w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
convert (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1

Result:
case h.e'_3
N : ℕ
inst✝ : NeZero N
⊢ (fun w => w * LFunctionTrivChar N (1 + w)) = (fun s => (s - 1) * LFunctionTrivChar N s) ∘ fun w => 1 + w

case convert_2
N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)

Proof state:
case convert_2
N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)

Tactic:
simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
  ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le

Result:
no goals
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem tendsto_leftLim_within (x : α) : Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)

Tactic:
filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_rel {l : Array α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (Array.foldr (fun a acc => f a acc) a l) (Array.foldr (fun a acc => g a acc) b l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (Array.foldr (fun a acc => f a acc) a { toList := l }) (Array.foldr (fun a acc => g a acc) b { toList := l })

Proof state:
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')

Tactic:
simpa using h'

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f g : α → β → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (Array.foldr (fun a acc => f a acc) a { toList := l }) (Array.foldr (fun a acc => g a acc) b { toList := l })

Tactic:
simpa using List.foldr_rel r h (by simpa using h')

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem ZMod.erdos_ginzburg_ziv_multiset (s : Multiset (ZMod n))
    (hs : 2 * n - 1 ≤ Multiset.card s) : ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0

Proof state:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs

Result:
no goals

Proof state:
case intro.intro
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0

Tactic:
exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩

Result:
no goals

Proof state:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0

Tactic:
obtain ⟨t, hts, ht⟩ := ZMod.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)

Result:
case intro.intro
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0

Proof state:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (Multiset.map Prod.fst t.val).sum = 0

Tactic:
simpa using ht

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformContinuous_of_continuousAt_one {hom : Type*} [UniformSpace β] [Group β]
    [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β]
    (f : hom) (hf : ContinuousAt f 1) :
    UniformContinuous f :=
  uniformContinuous_of_tendsto_one (by simpa using hf.tendsto)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : ContinuousAt (⇑f) 1
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
simpa using hf.tendsto

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem toLaurent_support (f : R[X]) : f.toLaurent.support = f.support.map Nat.castEmbedding

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)

Tactic:
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T,
  support_add_eq, Finset.insert_eq]

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (C (f.coeff a) * T ↑a).support ∪ (toLaurent (Polynomial.erase a f)).support =
    {Nat.castEmbedding a} ∪ (toLaurent (Polynomial.erase a f)).support

case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (C (f.coeff a) * T ↑a).support (toLaurent (Polynomial.erase a f)).support

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), f.support = ∅ → (toLaurent f).support = Finset.map Nat.castEmbedding ∅

Tactic:
intro f hf

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.support = ∅
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding ∅
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_right' :
    a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c :=
  calc
    a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Tactic:
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]

Result:
no goals

Proof state:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Tactic:
apply inf_left_right_swap

Result:
no goals

Proof state:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ

Tactic:
congr 1

Result:
case e_a.e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ

Proof state:
case e_a.e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ

Tactic:
rw [inf_comm, inf_assoc]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

Tactic:
congr 1

Result:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ

case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ

Tactic:
rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem sum_eq_zero_of_ne_one [IsDomain R'] {χ : MulChar R R'} (hχ : χ ≠ 1) : ∑ a, χ a = 0

Proof state:
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ ∑ a : R, χ a = 0

Tactic:
rcases ne_one_iff.mp hχ with ⟨b, hb⟩

Result:
case intro
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ ∑ a : R, χ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ ∑ a : R, χ a = 0

Tactic:
refine eq_zero_of_mul_eq_self_left hb ?_

Result:
case intro
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ χ ↑b * ∑ a : R, χ a = ∑ a : R, χ a

Proof state:
case intro
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : χ ↑b ≠ 1
⊢ χ ↑b * ∑ a : R, χ a = ∑ a : R, χ a

Tactic:
simpa only [Finset.mul_sum, ← map_mul] using b.mulLeft_bijective.sum_comp _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_nnreal_smul (m : ℝ≥0∞ → ℝ≥0∞) {c : ℝ≥0} (hc : c ≠ 0) :
    (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0
hc : c ≠ 0
⊢ mkMetric (c • m) = c • mkMetric m

Tactic:
rw [ENNReal.smul_def, ENNReal.smul_def,
  mkMetric_smul m ENNReal.coe_ne_top (ENNReal.coe_ne_zero.mpr hc)]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem card_normalizer_modEq_card [Finite G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime] {H : Subgroup G}
    (hH : Nat.card H = p ^ n) : Nat.card (normalizer H) ≡ Nat.card G [MOD p ^ (n + 1)]

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf H.normalizer) ≃ ↥H
⊢ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p * p ^ n]

Tactic:
exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf H.normalizer) ≃ ↥H
⊢ Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
rw [card_eq_card_quotient_mul_card_subgroup H,
  card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)), Nat.card_congr this,
  hH, pow_succ']

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf H.normalizer) ≃ ↥H
⊢ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p * p ^ n]

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf H.normalizer) ≃ ↥H
⊢ Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]
-- Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
lemma isHomLift {a : 𝒳.obj} {S : 𝒮} (ha : 𝒳.p.obj a = S) :
    IsHomLift 𝒴.p (𝟙 S) (α.toNatTrans.app a)

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)

Tactic:
infer_instance

Result:
no goals

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)

Tactic:
subst ha

Result:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)
-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
lemma shortExact_iff_of_iso (e : S₁ ≅ S₂) : S₁.ShortExact ↔ S₂.ShortExact

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.ShortExact → S₂.ShortExact

Tactic:
exact shortExact_of_iso e

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.ShortExact ↔ S₂.ShortExact

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.ShortExact → S₂.ShortExact

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₂.ShortExact → S₁.ShortExact

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₂.ShortExact → S₁.ShortExact

Tactic:
exact shortExact_of_iso e.symm

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
@[to_additive]
lemma mgraph_eq_mrange_prod (f : G →* H) : f.mgraph = mrange ((id _).prod f)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
⊢ f.mgraph = mrange ((id G).prod f)

Tactic:
aesop

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_false : Xor' False = id

Proof state:
⊢ Xor' False = id

Tactic:
ext

Result:
case h.a
x✝ : Prop
⊢ Xor' False x✝ ↔ id x✝

Proof state:
case h.a
x✝ : Prop
⊢ Xor' False x✝ ↔ id x✝

Tactic:
simp [Xor']

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem HasFPowerSeriesAt.comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hg : HasFPowerSeriesAt g q (f x)) (hf : HasFPowerSeriesAt f p x) :
    HasFPowerSeriesAt (g ∘ f) (q.comp p) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ Set.MapsTo f Set.univ Set.univ

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFPowerSeriesAt g q (f x)
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt (g ∘ f) (q.comp p) x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf hg ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFPowerSeriesWithinAt g q Set.univ (f x)
hf : HasFPowerSeriesWithinAt f p Set.univ x
⊢ HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) Set.univ x

Tactic:
apply hg.comp hf (by simp)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Indization/Category.lean
theorem Ind.exists_nonempty_arrow_mk_iso_ind_lim {A B : Ind C} {f : A ⟶ B} :
    ∃ (I : Type v) (_ : SmallCategory I) (_ : IsFiltered I) (F G : I ⥤ C) (φ : F ⟶ G),
      Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim _).map φ))

Proof state:
case intro.refine_3
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero).hom ≫
      (Arrow.mk ((Ind.lim P.I).map P.φ)).hom =
    (Arrow.mk f).hom ≫ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one).hom

Tactic:
simpa using
  (P.parallelPairIsoParallelPairCompIndYoneda.hom.naturality WalkingParallelPairHom.left).symm

Result:
no goals

Proof state:
case intro.refine_1
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).left ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).left

Tactic:
exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
⊢ ∃ I x, ∃ (x_1 : IsFiltered I), ∃ F G φ, Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map φ))

Tactic:
obtain ⟨P⟩ := nonempty_indParallelPairPresentation A.2 B.2
  (Ind.inclusion _ |>.map f) (Ind.inclusion _ |>.map f)

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ ∃ I x, ∃ (x_1 : IsFiltered I), ∃ F G φ, Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map φ))

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ ∃ I x, ∃ (x_1 : IsFiltered I), ∃ F G φ, Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map φ))

Tactic:
refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩

Result:
case intro.refine_1
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).left ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).left

case intro.refine_2
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).right ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).right

case intro.refine_3
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ Iso.hom ?intro.refine_1 ≫ (Arrow.mk ((Ind.lim P.I).map P.φ)).hom = (Arrow.mk f).hom ≫ Iso.hom ?intro.refine_2

Proof state:
case intro.refine_2
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).right ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).right

Tactic:
exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.isRepresentation.toEnd_surjective :
    Function.Surjective (Matrix.isRepresentation.toEnd R b hb)

Proof state:
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_2
inst✝³ : AddCommGroup M✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M✝
b : ι → M✝
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M✝
M : ↥(isRepresentation R b)
e : (toEnd R b hb) M = f
⊢ ∃ a, (toEnd R b hb) a = f

Tactic:
exact ⟨M, e⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Surjective ⇑(toEnd R b hb)

Tactic:
intro f

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
⊢ ∃ a, (toEnd R b hb) a = f

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
⊢ ∃ a, (toEnd R b hb) a = f

Tactic:
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)

Result:
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_2
inst✝³ : AddCommGroup M✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M✝
b : ι → M✝
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M✝
M : ↥(isRepresentation R b)
e : (toEnd R b hb) M = f
⊢ ∃ a, (toEnd R b hb) a = f

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
⊢ LinearMap.range f ≤ ⊤ • ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_le_le_eq_Icc [DecidablePred fun j => a ≤ j ∧ j ≤ b] :
    ({j | a ≤ j ∧ j ≤ b} : Finset _) = Icc a b

Proof state:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j ≤ b) univ ↔ a✝ ∈ Icc a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
⊢ filter (fun j => a ≤ j ∧ j ≤ b) univ = Icc a b

Tactic:
ext

Result:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j ≤ b) univ ↔ a✝ ∈ Icc a b