harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem isInducing_prodMap {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : IsInducing f)
    (hg : IsInducing g) : IsInducing (Limits.prod.map f g)

Proof state:
case eq_induced
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ (W ⨯ Y).str = induced (⇑(ConcreteCategory.hom (prod.map f g))) (X ⨯ Z).str

Tactic:
simp_rw [prod_topology, induced_inf, induced_compose, ← coe_comp,
  prod.map_fst, prod.map_snd, coe_comp, ← induced_compose (g := f), ← induced_compose (g := g)]

Result:
case eq_induced
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) (induced (⇑(ConcreteCategory.hom f)) X.str) ⊓
      induced (⇑(ConcreteCategory.hom prod.snd)) (induced (⇑(ConcreteCategory.hom g)) Z.str)

Proof state:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ IsInducing ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
constructor

Result:
case eq_induced
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ (W ⨯ Y).str = induced (⇑(ConcreteCategory.hom (prod.map f g))) (X ⨯ Z).str

Proof state:
case eq_induced
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) (induced (⇑(ConcreteCategory.hom f)) X.str) ⊓
      induced (⇑(ConcreteCategory.hom prod.snd)) (induced (⇑(ConcreteCategory.hom g)) Z.str)

Tactic:
rw [← hf.eq_induced, ← hg.eq_induced]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_self (a : S) : mk (a : M) a = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S) (1, 1) (↑a, a)

Tactic:
exact one_rel a

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ 1 = mk (↑a) a

Tactic:
rw [← mk_one, mk_eq_mk_iff]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S) (1, 1) (↑a, a)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ mk (↑a) a = 1

Tactic:
symm

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ 1 = mk (↑a) a
-- Mathlib/Data/Nat/Init.lean
lemma pred_le_iff : pred m ≤ n ↔ m ≤ succ n :=
  ⟨le_succ_of_pred_le, by
    cases m
    · exact fun _ ↦ zero_le n
    · exact le_of_succ_le_succ⟩

Proof state:
case zero
n : ℕ
⊢ 0 ≤ n.succ → pred 0 ≤ n

Tactic:
exact fun _ ↦ zero_le n

Result:
no goals

Proof state:
case succ
n n✝ : ℕ
⊢ n✝ + 1 ≤ n.succ → (n✝ + 1).pred ≤ n

Tactic:
exact le_of_succ_le_succ

Result:
no goals

Proof state:
m n : ℕ
⊢ m ≤ n.succ → m.pred ≤ n

Tactic:
cases m

Result:
case zero
n : ℕ
⊢ 0 ≤ n.succ → pred 0 ≤ n

case succ
n n✝ : ℕ
⊢ n✝ + 1 ≤ n.succ → (n✝ + 1).pred ≤ n
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma card_pow_le : ∀ {n}, (s ^ n).card ≤ s.card ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ, pow_succ]; refine card_mul_le.trans (by gcongr; exact card_pow_le)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) * #s ≤ #s ^ n * #s

Tactic:
gcongr

Result:
case bc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) ≤ #s ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n * s) ≤ #s ^ n * #s

Proof state:
case bc
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) ≤ #s ^ n

Tactic:
exact card_pow_le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ #(s ^ 0) ≤ #s ^ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n * s) ≤ #s ^ n * #s

Tactic:
refine card_mul_le.trans (by gcongr; exact card_pow_le)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivAt_iff_isLittleO_nhds_zero :
    HasFDerivAt f f' x ↔ (fun h : E => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivAt f f' x ↔ (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h

Tactic:
rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO, ← map_add_left_nhds_zero x, isLittleO_map]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ ((fun x' => f x' - f x - f' (x' - x)) ∘ fun x_1 => x + x_1) =o[𝓝 0] ((fun x' => x' - x) ∘ fun x_1 => x + x_1) ↔
    (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ ((fun x' => f x' - f x - f' (x' - x)) ∘ fun x_1 => x + x_1) =o[𝓝 0] ((fun x' => x' - x) ∘ fun x_1 => x + x_1) ↔
    (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma localized'_smul (I : Submodule R R) :
    (I • M').localized' S p f = I.localized' S p (Algebra.linearMap R S) • M'.localized' S p f :=
  Submodule.restrictScalars_injective R _ _ <| by
    simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ restrictScalars R (localized' S p f (I • M')) =
    restrictScalars R (localized' S p (Algebra.linearMap R S) I • localized' S p f M')

Tactic:
simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_ite_eq_true_eq_true {p : Prop} [h : Decidable p] {b c : Bool} :
  ¬(ite p (b = true) (c = true)) ↔ (ite p (b = false) (c = false))

Proof state:
p : Prop
h : Decidable p
b c : Bool
⊢ (¬if p then b = true else c = true) ↔ if p then b = false else c = false

Tactic:
cases h with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
b c : Bool
p : p✝
⊢ (¬if p✝ then b = true else c = true) ↔ if p✝ then b = false else c = false

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {f' : ℝ → E} {C : ℝ}
    (hf : ∀ x ∈ Icc (0 : ℝ) 1, HasDerivWithinAt f (f' x) (Icc (0 : ℝ) 1) x)
    (bound : ∀ x ∈ Ico (0 : ℝ) 1, ‖f' x‖ ≤ C) : ‖f 1 - f 0‖ ≤ C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc 0 1, HasDerivWithinAt f (f' x) (Icc 0 1) x
bound : ∀ x ∈ Ico 0 1, ‖f' x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C

Tactic:
simpa only [sub_zero, mul_one] using
  norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
lemma isVonNBounded_pi_iff {𝕜 ι : Type*} {E : ι → Type*} [NormedDivisionRing 𝕜]
    [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
    {S : Set (∀ i, E i)} : IsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S)

Proof state:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)

Tactic:
simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
  smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
  ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem sInf_add {s : Set ℝ≥0∞} : sInf s + a = ⨅ b ∈ s, b + a

Proof state:
a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
simp [sInf_eq_iInf, iInf_add]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem nhds_nil : 𝓝 ([] : List α) = pure []

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ 𝓝 [] = pure []

Tactic:
rw [nhds_list, List.traverse_nil _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a

Proof state:
a : Nat
h : 0 ≠ 0
⊢ 0 < 0

Tactic:
contradiction

Result:
no goals

Proof state:
a✝ a : Nat
h : a + 1 ≠ 0
⊢ 0 < a + 1

Tactic:
apply Nat.zero_lt_succ

Result:
no goals

Proof state:
a : Nat
h : a ≠ 0
⊢ 0 < a

Tactic:
match a with
| 0 => contradiction
| a+1 => apply Nat.zero_lt_succ

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem int_cyclotomic_spec (n : ℕ) :
    map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
      (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Proof state:
case pos
n : ℕ
hzero : n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos,
  eq_self_iff_true, Polynomial.map_one, and_self_iff]

Result:
no goals

Proof state:
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) ⋯.choose = cyclotomic' n ℂ ∧ ⋯.choose.degree = (cyclotomic' n ℂ).degree ∧ ⋯.choose.Monic

Tactic:
exact (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec

Result:
no goals

Proof state:
n : ℕ
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
by_cases hzero : n = 0

Result:
case pos
n : ℕ
hzero : n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Proof state:
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
rw [int_cyclotomic_rw hzero]

Result:
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) ⋯.choose = cyclotomic' n ℂ ∧ ⋯.choose.degree = (cyclotomic' n ℂ).degree ∧ ⋯.choose.Monic
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_eq_coe_nat (n : ℕ) : (C ↑n : MvPolynomial σ R) = n

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ C ↑n = ↑n

Tactic:
induction n <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frontier_inter_subset (s t : Set X) :
    frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
simp only [inter_union_distrib_left, union_inter_distrib_right, inter_assoc,
  inter_comm (closure t)]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
    (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.orthogonal W = ⊥) :
    W = ⊤

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
this : W ⊔ B.orthogonal W = ⊤
⊢ W = ⊤

Tactic:
rwa [b₃, sup_bot_eq] at this

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
⊢ W = ⊤

Tactic:
have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
this : W ⊔ B.orthogonal W = ⊤
⊢ W = ⊤
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ioi_mul_Ici_subset' (a b : α) : Ioi a * Ici b ⊆ Ioi (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Ioi a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioi (a * b)

Tactic:
exact mul_lt_mul_of_lt_of_le hya hzb

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Ioi a * Ici b ⊆ Ioi (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Ioi a
z : α
hzb : z ∈ Ici b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioi (a * b)
-- Mathlib/CategoryTheory/Simple.lean
theorem Simple.not_isZero (X : C) [Simple X] : ¬IsZero X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬IsZero X

Tactic:
simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma iso_inv_app (Y : D) :
    (iso adj a).inv.app Y =
      adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
          G.map ((shiftFunctorCompIsoId D b a h).inv.app
              (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D b).map
                ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b
                  (by rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel])).hom.app
                    (F.obj (G.obj Y)))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app Y))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        ((G.map ((shiftFunctor D a).map (𝟙 ((F ⋙ shiftFunctor D (-a)).obj ((shiftFunctor C a).obj (G.obj Y))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y))))) ≫
          G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.183099, u_1} C
inst✝⁴ : Category.{?u.183103, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ a + b = 0

Tactic:
rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_addPolynomial :
    (W'.map f).toAffine.addPolynomial (f x) (f y) (f ℓ) = (W'.addPolynomial x y ℓ).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ (map W' f).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map f (W'.addPolynomial x y ℓ)

Tactic:
rw [addPolynomial, map_polynomial, eval_map, linePolynomial, addPolynomial, ← coe_mapRingHom,
  ← eval₂_hom, linePolynomial]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ eval₂ (mapRingHom f) (C (f ℓ) * (X - C (f x)) + C (f y)) W'.polynomial =
    eval₂ (mapRingHom f) ((mapRingHom f) (C ℓ * (X - C x) + C y)) W'.polynomial

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ eval₂ (mapRingHom f) (C (f ℓ) * (X - C (f x)) + C (f y)) W'.polynomial =
    eval₂ (mapRingHom f) ((mapRingHom f) (C ℓ * (X - C x) + C y)) W'.polynomial

Tactic:
map_simp

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₁_eq_zero' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂)
    (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁', i₂⟩ ≠ i₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
rw [totalAux.d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq_zero, comp_zero, smul_zero]

Result:
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂
⊢ c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂

Proof state:
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂
⊢ c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂

Tactic:
exact h'

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem exists_Icc_mem_subset_of_mem_nhdsLE [OrderTopology α] {a : α} {s : Set α}
    (hs : s ∈ 𝓝[≤] a) : ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≤] a
⊢ ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s

Tactic:
simpa only [dual_Icc, toDual.surjective.exists] using
  exists_Icc_mem_subset_of_mem_nhdsGE (α := αᵒᵈ) (a := toDual a) hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {l : Vector α n} {a₁ a₂} :
     l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)

Proof state:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : Array α
⊢ foldl op (op a₁ a₂) { toArray := l, size_toArray := ⋯ } = op a₁ (foldl op a₂ { toArray := l, size_toArray := ⋯ })

Tactic:
simp [Array.foldl_assoc]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
op : α → α → α
ha : Std.Associative op
l : Vector α n
a₁ a₂ : α
⊢ foldl op (op a₁ a₂) l = op a₁ (foldl op a₂ l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : Array α
⊢ foldl op (op a₁ a₂) { toArray := l, size_toArray := ⋯ } = op a₁ (foldl op a₂ { toArray := l, size_toArray := ⋯ })
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- The full set is a fixed block. -/
@[to_additive "The full set is a fixed block."]
lemma IsFixedBlock.univ : IsFixedBlock G (univ : Set X) := fun _ ↦ by simp

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x✝ : G
⊢ x✝ • Set.univ = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_polynomial : (W'.baseChange B).toJacobian.polynomial =
    MvPolynomial.map f (W'.baseChange A).toJacobian.polynomial

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toJacobian.polynomial = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomial

Tactic:
rw [← map_polynomial, map_baseChange]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_tail_succ : ∀ (v : Vector α n.succ) (i : Fin n), get (tail v) i = get v i.succ
  | ⟨a :: l, e⟩, ⟨i, h⟩ => by simp [get_eq_get_toList]; rfl

Proof state:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).toList[i] = l[i]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).get ⟨i, h⟩ = get ⟨a :: l, e⟩ ⟨i, h⟩.succ

Tactic:
simp [get_eq_get_toList]

Result:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).toList[i] = l[i]
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.mem_closure_iff (hI : M.Indep I) :
    x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

Proof state:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

Tactic:
rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]

Result:
no goals