harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc]
lemma triangleMapOfHomotopy_comm₂ :
    inr φ₁ ≫ mapOfHomotopy H = b ≫ inr φ₂

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ inr φ₁ ≫ mapOfHomotopy H = b ≫ inr φ₂

Tactic:
simp [mapOfHomotopy]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mul_left (a₁ a₂ : ℤ) (b : ℕ) : J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)

Proof state:
a₁ a₂ : ℤ
b : ℕ
⊢ J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)

Tactic:
simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _]

Result:
a₁ a₂ : ℤ
b : ℕ
⊢ (List.map (fun x => legendreSym (↑x) a₁ * legendreSym (↑x) a₂) b.primeFactorsList.attach).prod =
    (List.map (fun x => legendreSym (↑x) a₁) b.primeFactorsList.attach).prod *
      (List.map (fun x => legendreSym (↑x) a₂) b.primeFactorsList.attach).prod

Proof state:
a₁ a₂ : ℤ
b : ℕ
⊢ (List.map (fun x => legendreSym (↑x) a₁ * legendreSym (↑x) a₂) b.primeFactorsList.attach).prod =
    (List.map (fun x => legendreSym (↑x) a₁) b.primeFactorsList.attach).prod *
      (List.map (fun x => legendreSym (↑x) a₂) b.primeFactorsList.attach).prod

Tactic:
exact List.prod_map_mul (α := ℤ) (l := (primeFactorsList b).attach)
  (f := fun x ↦ @legendreSym x {out := prime_of_mem_primeFactorsList x.2} a₁)
  (g := fun x ↦ @legendreSym x {out := prime_of_mem_primeFactorsList x.2} a₂)

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma ofHom_lift :
    Cochain.ofHom (lift φ α β eq) = liftCochain φ α β (zero_add 1)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Cochain.ofHom (lift φ α β eq) = liftCochain φ (↑α) β ⋯

Tactic:
simp only [lift, Cocycle.cochain_ofHom_homOf_eq_coe, liftCocycle_coe]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem discreteTopology_iff_nhds_ne [TopologicalSpace α] :
    DiscreteTopology α ↔ ∀ x : α, 𝓝[≠] x = ⊥

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem InfIrred.ne_top (ha : InfIrred a) : a ≠ ⊤

Proof state:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfIrred ⊤
⊢ False

Tactic:
exact not_infIrred_top ha

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : SemilatticeInf α
a : α
inst✝ : OrderTop α
ha : InfIrred a
⊢ a ≠ ⊤

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfIrred ⊤
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_neg_add_le_left {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c

Proof state:
a b c : Int
h : -b + a ≤ c
⊢ a ≤ b + c

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a + -b ≤ c
⊢ a ≤ b + c

Proof state:
a b c : Int
h : a + -b ≤ c
⊢ a ≤ b + c

Tactic:
exact Int.le_add_of_sub_left_le h

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem prod_apply_inr_snd (i) : (b.prod b' (Sum.inr i)).2 = b' i :=
  b'.repr.injective <| by
    ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
      LinearEquiv.prod_apply, b'.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
      Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inr_injective

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ i : ι'
⊢ (b'.repr ((b.prod b') (Sum.inr i✝)).2) i = (b'.repr (b' i✝)) i

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
  LinearEquiv.prod_apply, b'.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
  Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp]

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ i : ι'
⊢ (single (Sum.inr i✝) 1) (Sum.inr i) = (single i✝ 1) i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ i : ι'
⊢ (single (Sum.inr i✝) 1) (Sum.inr i) = (single i✝ 1) i

Tactic:
apply Finsupp.single_apply_left Sum.inr_injective

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b'.repr ((b.prod b') (Sum.inr i)).2 = b'.repr (b' i)

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ i : ι'
⊢ (b'.repr ((b.prod b') (Sum.inr i✝)).2) i = (b'.repr (b' i✝)) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem length_insertIdx : ∀ n as, (insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length
  | 0, _ => by simp
  | n + 1, [] => by simp
  | n + 1, a :: as => by
    simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
    split <;> rfl

Proof state:
α : Type u
a : α
x✝ : List α
⊢ (insertIdx 0 a x✝).length = if 0 ≤ x✝.length then x✝.length + 1 else x✝.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a✝ : α
n : Nat
a : α
as : List α
⊢ (insertIdx (n + 1) a✝ (a :: as)).length = if n + 1 ≤ (a :: as).length then (a :: as).length + 1 else (a :: as).length

Tactic:
simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]

Result:
α : Type u
a✝ : α
n : Nat
a : α
as : List α
⊢ (if n ≤ as.length then as.length + 1 else as.length) + 1 = if n ≤ as.length then as.length + 1 + 1 else as.length + 1

Proof state:
α : Type u
a✝ : α
n : Nat
a : α
as : List α
⊢ (if n ≤ as.length then as.length + 1 else as.length) + 1 = if n ≤ as.length then as.length + 1 + 1 else as.length + 1

Tactic:
split <;> rfl

Result:
no goals

Proof state:
α : Type u
a : α
n : Nat
⊢ (insertIdx (n + 1) a []).length = if n + 1 ≤ [].length then [].length + 1 else [].length

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The sets of `s`-factored and of `s ∪ {N}`-factored numbers are the same when `N` is not prime.
See `Nat.equivProdNatFactoredNumbers` for when `N` is prime. -/
lemma factoredNumbers_insert (s : Finset ℕ) {N : ℕ} (hN : ¬ N.Prime) :
    factoredNumbers (insert N s) = factoredNumbers s

Proof state:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
⊢ factoredNumbers (insert N s) = factoredNumbers s

Tactic:
ext m

Result:
case h
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s

Proof state:
case h
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s

Tactic:
refine ⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩,
        fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩

Result:
case h
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
hm : m ∈ factoredNumbers (insert N s)
p : ℕ
hp : p ∈ m.primeFactorsList
⊢ p ∈ s

Proof state:
case h
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
hm : m ∈ factoredNumbers (insert N s)
p : ℕ
hp : p ∈ m.primeFactorsList
⊢ p ∈ s

Tactic:
exact Finset.mem_of_mem_insert_of_ne (hm.2 p hp)
  fun h ↦ hN <| h ▸ prime_of_mem_primeFactorsList hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a

Proof state:
a b : Int
⊢ b * a.fdiv b + a.fmod b = a

Tactic:
rw [Int.add_comm]

Result:
a b : Int
⊢ a.fmod b + b * a.fdiv b = a

Proof state:
a b : Int
⊢ a.fmod b + b * a.fdiv b = a

Tactic:
exact fmod_add_fdiv ..

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem casesOn1 {f} (m : ℕ) (hf : Nat.Primrec f) : Nat.Primrec (Nat.casesOn · m f) :=
  (prec1 m (hf.comp left)).of_eq <| by simp

Proof state:
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
⊢ ∀ (n : ℕ), Nat.rec m (fun y IH => f (unpair (Nat.pair y IH)).1) n = Nat.casesOn n m f

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem neg_subst {α} [Ring α] {n e t : α} (h1 : n * e = t) : n * -e = -t

Proof state:
α : Type u_1
inst✝ : Ring α
n e t : α
h1 : n * e = t
⊢ n * -e = -t

Tactic:
simp [*]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_mul : (I * J).map g = I.map g * J.map g

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (I * J) = map g I * map g J

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g ⟨↑I * ↑J, ⋯⟩ = ⟨↑(map g I) * ↑(map g J), ⋯⟩

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g ⟨↑I * ↑J, ⋯⟩ = ⟨↑(map g I) * ↑(map g J), ⋯⟩

Tactic:
exact coeToSubmodule_injective (Submodule.map_mul _ _ _)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_eq_iff {a b : α} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : ℤ, a - b = z :=
  ⟨fun h => by
    rw [← h]
    exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩,
   by
    rintro ⟨h₀, h₁, z, hz⟩
    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz,
      Int.cast_inj, floor_eq_iff, ← hz]
    constructor <;> simpa [sub_eq_add_neg, add_assoc] ⟩

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ (0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z) → fract a = b

Tactic:
rintro ⟨h₀, h₁, z, hz⟩

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ fract a = b

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1

Tactic:
constructor <;> simpa [sub_eq_add_neg, add_assoc]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ fract a = b

Tactic:
rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz,
  Int.cast_inj, floor_eq_iff, ← hz]

Result:
case intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : fract a = b
⊢ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z

Tactic:
rw [← h]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem curryLeft_compLinearMap {n : ℕ} (g : M₂'' →ₗ[R'] M'')
    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
    (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
  ext fun v => congr_arg f <| funext <| by
    refine Fin.cases ?_ ?_
    · rfl
    · simp

Proof state:
case refine_1
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
inst✝⁶ : CommSemiring R'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : AddCommMonoid N''
inst✝² : Module R' M''
inst✝¹ : Module R' M₂''
inst✝ : Module R' N''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : M'' [⋀^Fin n.succ]→ₗ[R'] N''
m : M₂''
v : Fin n → M₂''
⊢ ((fun x => g) 0) (Matrix.vecCons m v 0) = Matrix.vecCons (g m) (fun i => ((fun x => g) i) (v i)) 0

Tactic:
rfl

Result:
no goals

Proof state:
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
inst✝⁶ : CommSemiring R'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : AddCommMonoid N''
inst✝² : Module R' M''
inst✝¹ : Module R' M₂''
inst✝ : Module R' N''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : M'' [⋀^Fin n.succ]→ₗ[R'] N''
m : M₂''
v : Fin n → M₂''
⊢ ∀ (x : Fin n.succ), ((fun x => g) x) (Matrix.vecCons m v x) = Matrix.vecCons (g m) (fun i => ((fun x => g) i) (v i)) x

Tactic:
refine Fin.cases ?_ ?_

Result:
case refine_1
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
inst✝⁶ : CommSemiring R'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : AddCommMonoid N''
inst✝² : Module R' M''
inst✝¹ : Module R' M₂''
inst✝ : Module R' N''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : M'' [⋀^Fin n.succ]→ₗ[R'] N''
m : M₂''
v : Fin n → M₂''
⊢ ((fun x => g) 0) (Matrix.vecCons m v 0) = Matrix.vecCons (g m) (fun i => ((fun x => g) i) (v i)) 0

case refine_2
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
inst✝⁶ : CommSemiring R'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : AddCommMonoid N''
inst✝² : Module R' M''
inst✝¹ : Module R' M₂''
inst✝ : Module R' N''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : M'' [⋀^Fin n.succ]→ₗ[R'] N''
m : M₂''
v : Fin n → M₂''
⊢ ∀ (i : Fin n),
    ((fun x => g) i.succ) (Matrix.vecCons m v i.succ) = Matrix.vecCons (g m) (fun i => ((fun x => g) i) (v i)) i.succ

Proof state:
case refine_2
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
inst✝⁶ : CommSemiring R'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : AddCommMonoid N''
inst✝² : Module R' M''
inst✝¹ : Module R' M₂''
inst✝ : Module R' N''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : M'' [⋀^Fin n.succ]→ₗ[R'] N''
m : M₂''
v : Fin n → M₂''
⊢ ∀ (i : Fin n),
    ((fun x => g) i.succ) (Matrix.vecCons m v i.succ) = Matrix.vecCons (g m) (fun i => ((fun x => g) i) (v i)) i.succ

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel`. -/
lemma mul_inv_le_one : a * a⁻¹ ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a : α
⊢ a * a⁻¹ ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem generated_le_generatedNormal : generated X ≤ generatedNormal X

Proof state:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
⊢ generated X ≤ generatedNormal X

Tactic:
apply @sInf_le_sInf (Subgroupoid C) _

Result:
case h
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
⊢ {S | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} ⊆ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}

Proof state:
case h
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
⊢ {S | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} ⊆ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}

Tactic:
exact fun S ⟨h, _⟩ => h

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem Int.exists_prime_and_dvd {n : ℤ} (hn : n.natAbs ≠ 1) : ∃ p, Prime p ∧ p ∣ n

Proof state:
case intro.intro
n : ℤ
hn : n.natAbs ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ n.natAbs
⊢ ∃ p, Prime p ∧ p ∣ n

Tactic:
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.natCast_dvd.mpr pd⟩

Result:
no goals

Proof state:
n : ℤ
hn : n.natAbs ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n

Tactic:
obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn

Result:
case intro.intro
n : ℤ
hn : n.natAbs ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ n.natAbs
⊢ ∃ p, Prime p ∧ p ∣ n
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma id_apply (M : MonCat) (x : M) :
    (𝟙 M : M ⟶ M) x = x

Proof state:
M : MonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_setIfInBounds {l : Array α} {i : Nat} {a : α} :
    (l.setIfInBounds i a).mapIdx f = (l.mapIdx f).setIfInBounds i (f i a)

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : List α
⊢ mapIdx f ({ toList := l }.setIfInBounds i a) = (mapIdx f { toList := l }).setIfInBounds i (f i a)

Tactic:
simp [List.mapIdx_set]

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : Array α
i : Nat
a : α
⊢ mapIdx f (l.setIfInBounds i a) = (mapIdx f l).setIfInBounds i (f i a)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : List α
⊢ mapIdx f ({ toList := l }.setIfInBounds i a) = (mapIdx f { toList := l }).setIfInBounds i (f i a)
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem mul_coeff_zero (p q : R[X]) : coeff (p * q) 0 = coeff p 0 * coeff q 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).coeff 0 = p.coeff 0 * q.coeff 0

Tactic:
simp [coeff_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp] lemma enorm_one : ‖(1 : G)‖ₑ = 1

Proof state:
G : Type u_1
inst✝² : SeminormedAddCommGroup G
inst✝¹ : One G
inst✝ : NormOneClass G
⊢ ‖1‖ₑ = 1

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
lemma pullbackMk_surjective (x : ToType (pullback f₁ f₂)) :
    ∃ (x₁ : ToType X₁) (x₂ : ToType X₂) (h : f₁ x₁ = f₂ x₂), x = pullbackMk f₁ f₂ x₁ x₂ h

Proof state:
case intro.mk.mk
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x₁ : ToType X₁
x₂ : ToType X₂
h : (ConcreteCategory.hom f₁) (x₁, x₂).1 = (ConcreteCategory.hom f₂) (x₁, x₂).2
⊢ ∃ x₁_1 x₂_1,
    ∃ (h_1 : (ConcreteCategory.hom f₁) x₁_1 = (ConcreteCategory.hom f₂) x₂_1),
      (pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩ = pullbackMk f₁ f₂ x₁_1 x₂_1 h_1

Tactic:
exact ⟨x₁, x₂, h, rfl⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x : ToType (pullback f₁ f₂)
⊢ ∃ x₁ x₂, ∃ (h : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂), x = pullbackMk f₁ f₂ x₁ x₂ h

Tactic:
obtain ⟨⟨⟨x₁, x₂⟩, h⟩, rfl⟩ := (pullbackEquiv f₁ f₂).symm.surjective x

Result:
case intro.mk.mk
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x₁ : ToType X₁
x₂ : ToType X₂
h : (ConcreteCategory.hom f₁) (x₁, x₂).1 = (ConcreteCategory.hom f₂) (x₁, x₂).2
⊢ ∃ x₁_1 x₂_1,
    ∃ (h_1 : (ConcreteCategory.hom f₁) x₁_1 = (ConcreteCategory.hom f₂) x₂_1),
      (pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩ = pullbackMk f₁ f₂ x₁_1 x₂_1 h_1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_eq_default [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = false) : getKey! a l = default

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
a : α
h : getKey? a l = none
⊢ getKey! a l = default

Tactic:
rw [getKey!_eq_getKey?, h, Option.get!_none]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
a : α
h : containsKey a l = false
⊢ getKey! a l = default

Tactic:
rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
  Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
a : α
h : getKey? a l = none
⊢ getKey! a l = default
-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem locallyConvexSpace_induced {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F]
    (f : E →ₗ[𝕜] F) : @LocallyConvexSpace 𝕜 E _ _ _ (t.induced f)

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (comap (⇑f) (𝓝 (f x))).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)

Tactic:
exact (LocallyConvexSpace.convex_basis <| f x).comap f

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (𝓝 x).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)

Tactic:
rw [nhds_induced]

Result:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (comap (⇑f) (𝓝 (f x))).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
⊢ LocallyConvexSpace 𝕜 E

Tactic:
letI : TopologicalSpace E := t.induced f

Result:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
⊢ LocallyConvexSpace 𝕜 E

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
  (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
  hs.linear_preimage f

Result:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (𝓝 x).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)