harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Limits.lean
lemma isCompl_opensRange_inl_inr :
    IsCompl (coprod.inl : X ⟶ X ⨿ Y).opensRange (coprod.inr : Y ⟶ X ⨿ Y).opensRange

Proof state:
case a
X Y : Scheme
⊢ ↑(Scheme.Hom.opensRange coprod.inl ⊓ Scheme.Hom.opensRange coprod.inr) = ↑⊥ ∧
      ↑(Scheme.Hom.opensRange coprod.inl ⊔ Scheme.Hom.opensRange coprod.inr) = ↑⊤ ↔
    Set.range ⇑(ConcreteCategory.hom coprod.inl.base) ⊓ Set.range ⇑(ConcreteCategory.hom coprod.inr.base) = ⊥ ∧
      Set.range ⇑(ConcreteCategory.hom coprod.inl.base) ⊔ Set.range ⇑(ConcreteCategory.hom coprod.inr.base) = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case a
X Y : Scheme
⊢ IsCompl (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (Set.range ⇑(ConcreteCategory.hom coprod.inl.base)) (Set.range ⇑(ConcreteCategory.hom coprod.inr.base))

Tactic:
simp only [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

Result:
case a
X Y : Scheme
⊢ ↑(Scheme.Hom.opensRange coprod.inl ⊓ Scheme.Hom.opensRange coprod.inr) = ↑⊥ ∧
      ↑(Scheme.Hom.opensRange coprod.inl ⊔ Scheme.Hom.opensRange coprod.inr) = ↑⊤ ↔
    Set.range ⇑(ConcreteCategory.hom coprod.inl.base) ⊓ Set.range ⇑(ConcreteCategory.hom coprod.inr.base) = ⊥ ∧
      Set.range ⇑(ConcreteCategory.hom coprod.inl.base) ⊔ Set.range ⇑(ConcreteCategory.hom coprod.inr.base) = ⊤

Proof state:
X Y : Scheme
⊢ IsCompl (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr)

Tactic:
convert isCompl_range_inl_inr X Y

Result:
case a
X Y : Scheme
⊢ IsCompl (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (Set.range ⇑(ConcreteCategory.hom coprod.inl.base)) (Set.range ⇑(ConcreteCategory.hom coprod.inr.base))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) :
    (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j]

Proof state:
α : Type ?u.475327
a : Array α
i : Nat
hi : i < a.size
j : Nat
hj : j < a.size
v : α
⊢ j < (a.set i v hi).size

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
v : α
hj : i < a.size
⊢ (a.set i v hi)[i] = if i = i then v else a[i]

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
j : Nat
hj : j < a.size
v : α
h : i = j
⊢ (a.set i v hi)[j] = if i = j then v else a[j]

Tactic:
subst j

Result:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
v : α
hj : i < a.size
⊢ (a.set i v hi)[i] = if i = i then v else a[i]

Proof state:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
j : Nat
hj : j < a.size
v : α
h : ¬i = j
⊢ (a.set i v hi)[j] = if i = j then v else a[j]

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
hi : i < a.size
j : Nat
hj : j < a.size
v : α
⊢ (a.set i v hi)[j] = if i = j then v else a[j]

Tactic:
if h : i = j then subst j; simp [*] else simp [*]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem pred_succ (o) : pred (succ o) = o

Proof state:
o : Ordinal.{u_4}
h : ∃ a, succ o = succ a
⊢ (succ o).pred = o

Tactic:
simpa only [pred, dif_pos h] using (succ_injective <| Classical.choose_spec h).symm

Result:
no goals

Proof state:
o : Ordinal.{u_4}
⊢ (succ o).pred = o

Tactic:
have h : ∃ a, succ o = succ a := ⟨_, rfl⟩

Result:
o : Ordinal.{u_4}
h : ∃ a, succ o = succ a
⊢ (succ o).pred = o
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem continuous_sin : Continuous sin

Proof state:
⊢ Continuous sin

Tactic:
change Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2

Result:
⊢ Continuous fun z => (cexp (-z * I) - cexp (z * I)) * I / 2

Proof state:
⊢ Continuous fun z => (cexp (-z * I) - cexp (z * I)) * I / 2

Tactic:
continuity

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem dvd_iff_mod_eq_zero {m n : ZNum} : m ∣ n ↔ n % m = 0

Proof state:
m n : ZNum
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0

Tactic:
rfl

Result:
no goals

Proof state:
m n : ZNum
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]

Result:
m n : ZNum
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0
-- Mathlib/Order/Filter/Pointwise.lean
theorem pure_div_pure : (pure a : Filter α) / pure b = pure (a / b)

Proof state:
α : Type u_2
inst✝ : Div α
a b : α
⊢ pure a / pure b = pure (a / b)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/Irrational.lean
theorem eventually_forall_le_dist_cast_rat_of_den_le (hx : Irrational x) (n : ℕ) :
    ∀ᶠ ε : ℝ in 𝓝 0, ∀ r : ℚ, r.den ≤ n → ε ≤ dist x r :=
  (hx.eventually_forall_le_dist_cast_div_of_denom_le n).mono fun ε H r hr => by
    simpa only [Rat.cast_def] using H r.den hr r.num

Proof state:
x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x ↑r

Tactic:
simpa only [Rat.cast_def] using H r.den hr r.num

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_two : s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
case refine_2
α : Type u_1
s : Set α
h : s.encard = 2
⊢ ↑s.encard.toNat = 2

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ ↑s.encard.toNat = 2 ↔ s.encard = 2

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
⊢ s.encard = 2

case refine_2
α : Type u_1
s : Set α
h : s.encard = 2
⊢ ↑s.encard.toNat = 2

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
h' : s.encard = ⊤
⊢ False

Tactic:
simp [h'] at h

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
⊢ s.encard ≠ ⊤

Tactic:
rintro h'

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
h' : s.encard = ⊤
⊢ False

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
⊢ s.encard = 2

Tactic:
rwa [ENat.coe_toNat] at h

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 2
⊢ s.encard ≠ ⊤

Proof state:
α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [← encard_eq_two, ncard_def, ← Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]

Result:
α : Type u_1
s : Set α
⊢ ↑s.encard.toNat = 2 ↔ s.encard = 2
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem smul_extend {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    [NoZeroSMulDivisors R ℝ≥0∞] {c : R} (hc : c ≠ 0) :
    c • extend m = extend fun s h => c • m s h

Proof state:
case h
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h => c • m s h) s

Tactic:
dsimp [extend]

Result:
case h
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

Proof state:
case h
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

Tactic:
by_cases h : P s

Result:
case pos
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

case neg
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

Proof state:
case pos
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ c • ⨅ (h : P s), m s h = ⨅ (h : P s), c • m s h

Tactic:
simp [h, ENNReal.smul_top, hc]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
⊢ c • extend m = extend fun s h => c • m s h

Tactic:
ext1 s

Result:
case h
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
R : Type u_2
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h => c • m s h) s
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_nsmul (m : ℕ) (x : 𝕎 R) (n : ℕ) : init n (m • x) = init n (m • init n x)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem range_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    range (Basis.extendLe hs hst ht) = hs.extend hst

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : ⊤ ≤ span K t
⊢ range ⇑(extendLe hs hst ht) = hs.extend hst

Tactic:
rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals
-- Mathlib/RingTheory/Presentation.lean
@[simp]
lemma aeval_val_relation (i) : aeval P.val (P.relation i) = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Ideal.span (Set.range P.relation)

Tactic:
exact Ideal.subset_span ⟨i, rfl⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ (aeval P.val) (P.relation i) = 0

Tactic:
rw [← RingHom.mem_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Ideal.span (Set.range P.relation)
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem cons_add (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
    f (cons (x + y) m) = f (cons x m) + f (cons y m)

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
⊢ f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

Tactic:
simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred/WithBot.lean
@[simp]
lemma succ_one : succ (1 : WithBot α) = 2

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 1 = 2

Tactic:
simpa [one_add_one_eq_two] using succ_natCast 1

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_sub_le_iff_right (pn : p.natDegree ≤ n) :
    (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
rwa [natDegree_sub, natDegree_sub_le_iff_left]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem leadingCoeff_map [Semiring S] [Nontrivial S] (f : R →+* S) :
    leadingCoeff (p.map f) = f (leadingCoeff p)

Proof state:
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
simp only [← coeff_natDegree, coeff_map f, natDegree_map]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_union (s t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_iff : toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z : ℤ, b = c + z • p

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - n • p

Tactic:
rw [← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc, toIcoMod]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b - z • p = c) → toIcoMod hp a b = c

Tactic:
rintro ⟨hc, n, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - n • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
refine
  ⟨fun h =>
    ⟨h ▸ toIcoMod_mem_Ico hp a b, toIcoDiv hp a b, h ▸ (toIcoMod_add_toIcoDiv_zsmul _ _ _).symm⟩,
    ?_⟩

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b - z • p = c) → toIcoMod hp a b = c
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_neg (a b : α) : toIocMod hp a (-b) = p - toIcoMod hp (-a) b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (-b) = p - toIcoMod hp (-a) b

Tactic:
simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIcoDiv hp (-a) b • p + 1 • p) = p - (b - toIcoDiv hp (-a) b • p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIcoDiv hp (-a) b • p + 1 • p) = p - (b - toIcoDiv hp (-a) b • p)

Tactic:
abel

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem theory_model_iff (h : M ≅[L] N) : M ⊨ T ↔ N ⊨ T

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
  h.completeTheory_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : Nontrivial H ↔ ∃ x ∈ H, x ≠ (1 : G)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Basic.lean
theorem projective_of_preservesFiniteColimits_preadditiveCoyonedaObj (P : C)
    [hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)] : Projective P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
⊢ Projective P

Tactic:
rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
have := Functor.preservesHomologyOfExact (preadditiveCoyonedaObj P)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
this : (preadditiveCoyonedaObj P).PreservesHomology
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P)
this : (preadditiveCoyonedaObj P).PreservesHomology
⊢ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/Order/LawsonTopology.lean
lemma isLawson_le_isScott : L ≤ S

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ lawson α ≤ scott α univ

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ L ≤ S

Tactic:
rw [@IsScott.topology_eq α univ _ S _, @IsLawson.topology_eq_lawson α _ L _]

Result:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ lawson α ≤ scott α univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_fst_zip :
    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
  | [], _, _ => rfl
  | _ :: as, _ :: bs, h => by
    simp [Nat.succ_le_succ_iff] at h
    show _ :: map Prod.fst (zip as bs) = _ :: as
    rw [map_fst_zip as bs h]
  | _ :: _, [], h => by simp at h

Proof state:
α : Type u_1
β : Type u_2
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : as.length ≤ bs.length
⊢ map Prod.fst ((head✝¹ :: as).zip (head✝ :: bs)) = head✝¹ :: as

Tactic:
show _ :: map Prod.fst (zip as bs) = _ :: as

Result:
α : Type u_1
β : Type u_2
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : as.length ≤ bs.length
⊢ (head✝¹, head✝).fst :: map Prod.fst (as.zip bs) = head✝¹ :: as

Proof state:
α : Type u_1
β : Type u_2
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : (head✝¹ :: as).length ≤ (head✝ :: bs).length
⊢ map Prod.fst ((head✝¹ :: as).zip (head✝ :: bs)) = head✝¹ :: as

Tactic:
simp [Nat.succ_le_succ_iff] at h

Result:
α : Type u_1
β : Type u_2
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : as.length ≤ bs.length
⊢ map Prod.fst ((head✝¹ :: as).zip (head✝ :: bs)) = head✝¹ :: as

Proof state:
α : Type u_1
β : Type u_2
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length ≤ [].length
⊢ map Prod.fst ((head✝ :: tail✝).zip []) = head✝ :: tail✝

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
head✝¹ : α
as : List α
head✝ : β
bs : List β
h : as.length ≤ bs.length
⊢ (head✝¹, head✝).fst :: map Prod.fst (as.zip bs) = head✝¹ :: as

Tactic:
rw [map_fst_zip as bs h]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Proof state:
x : EReal
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Tactic:
cases x <;> norm_num

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_add_iff_of_nonpos {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ)
    (hf : f ≤ᵐ[μ] 0) (hg : g ≤ᵐ[μ] 0) :
    Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ

Tactic:
exact integrable_add_iff_of_nonneg h_meas.neg (hf.mono (fun _ ↦ neg_nonneg_of_nonpos))
  (hg.mono (fun _ ↦ neg_nonneg_of_nonpos))

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
rw [← integrable_neg_iff, ← integrable_neg_iff (f := f), ← integrable_neg_iff (f := g), neg_add]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem coe_eq_singleton {H : Subgroup G} : (∃ g : G, (H : Set G) = {g}) ↔ H = ⊥ :=
  ⟨fun ⟨g, hg⟩ =>
    haveI : Subsingleton (H : Set G)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H

Tactic:
rw [hg]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Group/Units/Equiv.lean
@[to_additive (attr := simp)]
lemma toUnits_val_apply {G : Type*} [Group G] (x : Gˣ) : toUnits (x : G) = x

Proof state:
G : Type u_6
inst✝ : Group G
x : Gˣ
⊢ toUnits ↑x = x

Tactic:
simp_rw [MulEquiv.apply_eq_iff_symm_apply, toUnits_symm_apply]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Field/Basic.lean
theorem FieldAxiom.realize_toSentence_iff_toProp {K : Type*}
    [Add K] [Mul K] [Neg K] [Zero K] [One K] [CompatibleRing K]
    (ax : FieldAxiom) :
    (K ⊨ (ax.toSentence : Sentence Language.ring)) ↔ ax.toProp K

Proof state:
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
ax : FieldAxiom
⊢ K ⊨ ax.toSentence ↔ toProp K ax

Tactic:
cases ax <;>
simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem JoinedIn.joined_subtype (h : JoinedIn F x y) :
    Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F) :=
  ⟨{  toFun := fun t => ⟨h.somePath t, h.somePath_mem t⟩
      continuous_toFun

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Continuous fun t => ⟨h.somePath t, ⋯⟩

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ { toFun := fun t => ⟨h.somePath t, ⋯⟩, continuous_toFun := ⋯ }.toFun 0 = ⟨x, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ { toFun := fun t => ⟨h.somePath t, ⋯⟩, continuous_toFun := ⋯ }.toFun 1 = ⟨y, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem isCoseparator_iff_faithful_preadditiveYoneda (G : C) :
    IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveYoneda.obj G ⋙ forget AddCommGrp).Faithful ↔ (preadditiveYoneda.obj G).Faithful

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrp),
  fun h => Functor.Faithful.comp _ _⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful

Tactic:
rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj,
  whiskeringRight_obj_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveYoneda.obj G ⋙ forget AddCommGrp).Faithful ↔ (preadditiveYoneda.obj G).Faithful