harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma dvd_mul_sub_mul_mul_gcd_of_dvd {p a b c d x y : R} [IsDomain R] [GCDMonoid R]
    (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * gcd x y

Proof state:
R : Type u_1
inst✝² : CommRing R
p a b c d x y : R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ gcd ((a * d - b * c) * x) ((a * d - b * c) * y)

Tactic:
exact (dvd_gcd_iff _ _ _).2 ⟨dvd_mul_sub_mul_mul_left_of_dvd h1 h2,
  dvd_mul_sub_mul_mul_right_of_dvd h1 h2⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
p a b c d x y : R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * gcd x y

Tactic:
rw [← (gcd_mul_left' (a*d - b*c) x y).dvd_iff_dvd_right]

Result:
R : Type u_1
inst✝² : CommRing R
p a b c d x y : R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ gcd ((a * d - b * c) * x) ((a * d - b * c) * y)
-- Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
theorem colimit_one_eq (j : J) : (1 : M.{v, u} F) = M.mk F ⟨j, 1⟩

Proof state:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ 1 = M.mk F ⟨j, 1⟩

Tactic:
apply M.mk_eq

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨⋯.some, 1⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨j, 1⟩.snd

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨⋯.some, 1⟩.fst j))) ⟨⋯.some, 1⟩.snd =
    (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨⋯.some, 1⟩.fst j))) ⟨j, 1⟩.snd

Tactic:
simp

Result:
no goals

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨⋯.some, 1⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨j, 1⟩.snd

Tactic:
refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨⋯.some, 1⟩.fst j))) ⟨⋯.some, 1⟩.snd =
    (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨⋯.some, 1⟩.fst j))) ⟨j, 1⟩.snd
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparisonNatTrans_comp {E : Type u₂} [Category.{v₂} E] [ChosenFiniteProducts E]
    (G : D ⥤ E) : prodComparisonNatTrans (F ⋙ G) A =
      whiskerRight (prodComparisonNatTrans F A) G ≫
        whiskerLeft F (prodComparisonNatTrans G (F.obj A))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
⊢ prodComparisonNatTrans (F ⋙ G) A =
    whiskerRight (prodComparisonNatTrans F A) G ≫ whiskerLeft F (prodComparisonNatTrans G (F.obj A))

Tactic:
ext

Result:
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
x✝ : C
⊢ (prodComparisonNatTrans (F ⋙ G) A).app x✝ =
    (whiskerRight (prodComparisonNatTrans F A) G ≫ whiskerLeft F (prodComparisonNatTrans G (F.obj A))).app x✝

Proof state:
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
x✝ : C
⊢ (prodComparisonNatTrans (F ⋙ G) A).app x✝ =
    (whiskerRight (prodComparisonNatTrans F A) G ≫ whiskerLeft F (prodComparisonNatTrans G (F.obj A))).app x✝

Tactic:
simp [prodComparison_comp]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem principal_isMeasurablyGenerated_iff {s : Set α} :
    IsMeasurablyGenerated (𝓟 s) ↔ MeasurableSet s

Proof state:
case mk
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s

Tactic:
rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩

Result:
case mk.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s

Proof state:
case mk.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s

Tactic:
rwa [← this]

Result:
no goals

Proof state:
case mk.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s

Tactic:
have : t = s := hts.antisymm ht

Result:
case mk.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated → MeasurableSet s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated → MeasurableSet s

Tactic:
rintro ⟨hs⟩

Result:
case mk
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s
-- Mathlib/Data/PNat/Prime.lean
theorem dvd_prime {p m : ℕ+} (pp : p.Prime) : m ∣ p ↔ m = 1 ∨ m = p

Proof state:
p m : ℕ+
pp : p.Prime
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p

Tactic:
simp

Result:
no goals

Proof state:
p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p

Tactic:
rw [Nat.dvd_prime pp]

Result:
p m : ℕ+
pp : p.Prime
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p

Proof state:
p m : ℕ+
pp : p.Prime
⊢ m ∣ p ↔ m = 1 ∨ m = p

Tactic:
rw [PNat.dvd_iff]

Result:
p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem Prime.not_weird (h : Prime n) : ¬ Weird n

Proof state:
n : ℕ
h : Prime n
⊢ ¬n.Abundant ∨ ¬¬n.Pseudoperfect

Tactic:
left

Result:
case h
n : ℕ
h : Prime n
⊢ ¬n.Abundant

Proof state:
case h
n : ℕ
h : Prime n
⊢ ¬n.Abundant

Tactic:
exact h.not_abundant

Result:
no goals

Proof state:
n : ℕ
h : Prime n
⊢ ¬n.Weird

Tactic:
simp only [Nat.Weird, not_and_or]

Result:
n : ℕ
h : Prime n
⊢ ¬n.Abundant ∨ ¬¬n.Pseudoperfect
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[bound]
lemma mul_inv_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1 :=
  mul_inv_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ 1 * b

Tactic:
rwa [one_mul]

Result:
no goals
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem BaireMeasurableSet.preimage (hc : Continuous f) (ho : IsOpenMap f)
    {s : Set β} (h : BaireMeasurableSet s) : BaireMeasurableSet (f⁻¹' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this✝³ : MeasurableSpace α := borel α
this✝² : BorelSpace α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (f ⁻¹' u)

Tactic:
exact hc.measurable hu

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
refine ⟨f ⁻¹' u, ?_, hsu.filter_mono <| tendsto_residual_of_isOpenMap hc ho⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ MeasurableSet (f ⁻¹' u)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s : Set β
h : BaireMeasurableSet s
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
rcases h with ⟨u, hu, hsu⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ BaireMeasurableSet (f ⁻¹' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ MeasurableSet (f ⁻¹' u)

Tactic:
borelize α β

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hc : Continuous f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this✝³ : MeasurableSpace α := borel α
this✝² : BorelSpace α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (f ⁻¹' u)
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma ι₁_π : ι₁ K ≫ π K = 𝟙 K

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
⊢ ι₁ K ≫ π K = 𝟙 K

Tactic:
simp [π]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : Array α) :
    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
l : Array α
⊢ filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
toList✝ : List α
⊢ filterMap g (filterMap f { toList := toList✝ }) = filterMap (fun x => (f x).bind g) { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
toList✝ : List α
⊢ filterMap g (filterMap f { toList := toList✝ }) = filterMap (fun x => (f x).bind g) { toList := toList✝ }

Tactic:
simp [List.filterMap_filterMap]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sub_limZero {f g : CauSeq β abv} (hf : LimZero f) (hg : LimZero g) : LimZero (f - g)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f.LimZero
hg : g.LimZero
⊢ (f - g).LimZero

Tactic:
simpa only [sub_eq_add_neg] using add_limZero hf (neg_limZero hg)

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem isStoppingTime_hitting_isStoppingTime [ConditionallyCompleteLinearOrder ι]
    [WellFoundedLT ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι]
    [FirstCountableTopology ι] [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace β]
    [BorelSpace β] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → ι} (hτ : IsStoppingTime f τ)
    {N : ι} (hτbdd : ∀ x, τ x ≤ N) {s : Set β} (hs : MeasurableSet s) (hf : Adapted f u) :
    IsStoppingTime f fun x => hitting u s (τ x) N x

Proof state:
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
x : Ω
hm : n < τ x
⊢ n < hitting u s (τ x) N x

Tactic:
exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _)

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : ConditionallyCompleteLinearOrder ι
inst✝⁸ : WellFoundedLT ι
inst✝⁷ : Countable ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
inst✝⁴ : FirstCountableTopology ι
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ N
s : Set β
hs : MeasurableSet s
hf : Adapted f u
n : ι
h₁ :
  {x | hitting u s (τ x) N x ≤ n} =
    (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
      ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}
h₂ : ⋃ i, ⋃ (_ : i > n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅
⊢ MeasurableSet (⋃ i, ⋃ (_ : i ≤ n), {x | τ x = i} ∩ {x | hitting u s i N x ≤ n})

Tactic:
exact MeasurableSet.iUnion fun i => MeasurableSet.iUnion fun hi =>
  (f.mono hi _ (hτ.measurableSet_eq i)).inter (hitting_isStoppingTime hf hs n)

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Field.lean
theorem one_div_le_one_div {n m : ℕ} (h : n ≤ m) : 1 / ((m : α) + 1) ≤ 1 / ((n : α) + 1)

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1

Tactic:
simpa

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1

Tactic:
exact Nat.cast_add_one_pos _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)

Tactic:
refine one_div_le_one_div_of_le ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1

case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :
    (as ++ bs)[i] = as[i]

Proof state:
α : Type u_1
i : Nat
as bs : List α
h : i < as.length
h' : i < (as ++ bs).length
⊢ (as ++ bs)[i] = as[i]

Tactic:
induction as generalizing i with
| nil => trivial
| cons a as ih =>
  cases i with
  | zero => rfl
  | succ i => apply ih

Result:
no goals

Proof state:
case nil
α : Type u_1
bs : List α
i : Nat
h : i < [].length
h' : i < ([] ++ bs).length
⊢ ([] ++ bs)[i] = [][i]

Tactic:
trivial

Result:
no goals

Proof state:
case cons
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h : i < as.length) {h' : i < (as ++ bs).length}, (as ++ bs)[i] = as[i]
i : Nat
h : i < (a :: as).length
h' : i < (a :: as ++ bs).length
⊢ (a :: as ++ bs)[i] = (a :: as)[i]

Tactic:
cases i with
| zero => rfl
| succ i => apply ih

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h : i < as.length) {h' : i < (as ++ bs).length}, (as ++ bs)[i] = as[i]
h : 0 < (a :: as).length
h' : 0 < (a :: as ++ bs).length
⊢ (a :: as ++ bs)[0] = (a :: as)[0]

Tactic:
rfl

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h : i < as.length) {h' : i < (as ++ bs).length}, (as ++ bs)[i] = as[i]
i : Nat
h : i + 1 < (a :: as).length
h' : i + 1 < (a :: as ++ bs).length
⊢ (a :: as ++ bs)[i + 1] = (a :: as)[i + 1]

Tactic:
apply ih

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean
theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion g]
    [IsImmersion (f ≫ g)] : IsImmersion f where
  __ := IsPreimmersion.of_comp f g
  isLocallyClosed_range

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsImmersion g
inst✝ : IsImmersion (f ≫ g)
this : IsLocallyClosed ((TopCat.Hom.hom g.base).toFun ⁻¹' Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
⊢ IsLocallyClosed
    (⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base)))

Tactic:
simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] using this

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsImmersion g
inst✝ : IsImmersion (f ≫ g)
⊢ IsLocallyClosed
    (⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base)))

Tactic:
have := (f ≫ g).isLocallyClosed_range.preimage g.base.hom.2

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsImmersion g
inst✝ : IsImmersion (f ≫ g)
this : IsLocallyClosed ((TopCat.Hom.hom g.base).toFun ⁻¹' Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
⊢ IsLocallyClosed
    (⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base)))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsImmersion g
inst✝ : IsImmersion (f ≫ g)
⊢ IsLocallyClosed (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
rw [← Set.preimage_image_eq (Set.range _) g.isEmbedding.injective]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsImmersion g
inst✝ : IsImmersion (f ≫ g)
⊢ IsLocallyClosed
    (⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base)))
-- Mathlib/CategoryTheory/Opposites.lean
@[reassoc (attr := simp)]
lemma unop_hom_inv_id_app : (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))

Tactic:
rw [← unop_comp, inv_hom_id_app, unop_id]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem convex_closedBall : Convex ℝ (closedBall p x r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)

Tactic:
exact convex_iInter₂ fun _ _ => convex_ball _ _ _

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (p.closedBall x r)

Tactic:
rw [closedBall_eq_biInter_ball]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)
-- Mathlib/Order/Bounds/Basic.lean
theorem isLeast_sdiff [GeneralizedCoheytingAlgebra α] (a b : α) :
    IsLeast {w | a ≤ b ⊔ w} (a \ b)

Proof state:
α : Type u
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ IsLeast {w | a ≤ b ⊔ w} (a \ b)

Tactic:
simp [IsLeast, mem_lowerBounds]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
lemma toPartENat_le_iff_of_le_aleph0 {c c' : Cardinal} (h : c ≤ ℵ₀) :
    toPartENat c ≤ toPartENat c' ↔ c ≤ c'

Proof state:
case intro
c' : Cardinal.{u_1}
c : ℕ∞
⊢ toPartENat ↑c ≤ toPartENat c' ↔ ↑c ≤ c'

Tactic:
simp_rw [← partENatOfENat_toENat, toENat_ofENat, enat_gc _,
 ← PartENat.withTopOrderIso.symm.le_iff_le, PartENat.ofENat_le, map_le_map_iff]

Result:
no goals

Proof state:
c c' : Cardinal.{u_1}
h : c ≤ ℵ₀
⊢ toPartENat c ≤ toPartENat c' ↔ c ≤ c'

Tactic:
lift c to ℕ∞ using h

Result:
case intro
c' : Cardinal.{u_1}
c : ℕ∞
⊢ toPartENat ↑c ≤ toPartENat c' ↔ ↑c ≤ c'
-- Mathlib/Data/Nat/Factors.lean
theorem dvd_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ∣ n

Proof state:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Tactic:
rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

Result:
no goals

Proof state:
n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ∣ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Proof state:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem ones_embedding (i : Fin (ones n).length) (h : 0 < (ones n).blocksFun i) :
    (ones n).embedding i ⟨0, h⟩ = ⟨i, lt_of_lt_of_le i.2 (ones n).length_le⟩

Proof state:
case h
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ↑(((ones n).embedding i) ⟨0, h⟩) = ↑⟨↑i, ⋯⟩

Tactic:
simpa using i.2.le

Result:
no goals

Proof state:
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ((ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩

Tactic:
ext

Result:
case h
n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ↑(((ones n).embedding i) ⟨0, h⟩) = ↑⟨↑i, ⋯⟩
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma EdgeDisjointTriangles.map (f : α ↪ β) (hG : G.EdgeDisjointTriangles) :
    (G.map f).EdgeDisjointTriangles

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y => (↑x ∩ ↑y).Subsingleton) (Finset.map f))

Tactic:
rintro s hs t ht hst

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ Function.onFun (fun x y => (↑x ∩ ↑y).Subsingleton) (Finset.map f) s t

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y => (↑x ∩ ↑y).Subsingleton) (Finset.map f))

Tactic:
classical
rintro s hs t ht hst
dsimp [Function.onFun]
rw [← coe_inter, ← map_inter, coe_map, coe_inter]
exact (hG hs ht hst).image _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ Function.onFun (fun x y => (↑x ∩ ↑y).Subsingleton) (Finset.map f) s t

Tactic:
dsimp [Function.onFun]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f s) ∩ ↑(Finset.map f t)).Subsingleton

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton

Tactic:
exact (hG hs ht hst).image _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (SimpleGraph.map f G).EdgeDisjointTriangles

Tactic:
rw [EdgeDisjointTriangles, cliqueSet_map (by norm_num : 3 ≠ 1),
  (Finset.map_injective f).injOn.pairwise_image]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y => (↑x ∩ ↑y).Subsingleton) (Finset.map f))

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ 3 ≠ 1

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (↑(Finset.map f s) ∩ ↑(Finset.map f t)).Subsingleton

Tactic:
rw [← coe_inter, ← map_inter, coe_map, coe_inter]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton