harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem not_linearIndependent_pair_of_commute_of_flat_left [Module.Flat R M]
    (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) : ¬LinearIndependent R ![a, b] := fun h ↦ by
  let n : Fin 2 → N := (inclusion inf_le_right) ∘ ![a, b]
  have hn : LinearIndependent R n := h.map' _ (ker_inclusion _ _ _)
  -- need this instance otherwise it only has semigroup structure
  letI : AddCommGroup (Fin 2 →₀ M) := Finsupp.instAddCommGroup
  let m : Fin 2 →₀ M := .single 0 ⟨b.1, b.2.1⟩ - .single 1 ⟨a.1, a.2.1⟩
  have hm : mulRightMap M n m = 0

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
⊢ False

Tactic:
let n : Fin 2 → N := (inclusion inf_le_right) ∘ ![a, b]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
⊢ False

Tactic:
have hm : mulRightMap M n m = 0 := by simp [m, n, show _ * _ = _ * _ from hc]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : (M.mulRightMap n) m = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Module.Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : b = 0 ∧ a = 0
⊢ False

Tactic:
exact h.ne_zero 0 hm.2

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
/-- If `m` is a subadditive function (`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division
by a natural, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
lemma le_expect_of_subadditive (h_zero : m 0 = 0) (h_add : ∀ a b, m (a + b) ≤ m a + m b)
    (h_div : ∀ (n : ℕ) a, m (a /ℚ n) = m a /ℚ n) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
  le_expect_of_subadditive_on_pred (p := fun _ ↦ True) h_zero (by simpa) (by simp) (by simpa)
    (by simp)

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (n : ℕ) (a : M), (fun x => True) a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (a b : M), (fun x => True) a → (fun x => True) b → m (a + b) ≤ m a + m b

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ i ∈ s, (fun x => True) (f i)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (a b : M), (fun x => True) a → (fun x => True) b → (fun x => True) (a + b)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_X :
    d.mapCoeffs (X : A[X]) = 0

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
⊢ d.mapCoeffs X = 0

Tactic:
simp [← monomial_one_one_eq_X]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem image_ι_eq {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ image φ} [Epi e]
    {i : image φ ⟶ Δ''} [Mono i] (fac : e ≫ i = φ) : image.ι φ = i

Proof state:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image.ι φ = i

Tactic:
haveI := strongEpi_of_epi e

Result:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image.ι φ = i

Proof state:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image.ι φ = i

Tactic:
rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
  SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
lemma Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹)
    {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}

Proof state:
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
⊢ InvOn (fun x => x * (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}

Tactic:
constructor <;> intro x (hx : x < 1)

Result:
case left
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x => x * (1 + x)⁻¹) ((fun x => x * (1 - x)⁻¹) x) = x

case right
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x => x * (1 - x)⁻¹) ((fun x => x * (1 + x)⁻¹) x) = x

Proof state:
case right
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x => x * (1 - x)⁻¹) ((fun x => x * (1 + x)⁻¹) x) = x

Tactic:
field_simp [mul_tsub]

Result:
no goals

Proof state:
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
⊢ InvOn (fun x => 1 - (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}

Tactic:
rw [← this]

Result:
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
⊢ InvOn (fun x => x * (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}

Proof state:
case h
x : ℝ≥0
⊢ x = (1 - 1 / (1 + x)) * (1 + x)

Tactic:
simp [tsub_mul, inv_mul_cancel₀]

Result:
no goals

Proof state:
case left
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x => x * (1 + x)⁻¹) ((fun x => x * (1 - x)⁻¹) x) = x

Tactic:
have : 0 < 1 - x := tsub_pos_of_lt hx

Result:
case left
this✝ : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
this : 0 < 1 - x
⊢ (fun x => x * (1 + x)⁻¹) ((fun x => x * (1 - x)⁻¹) x) = x

Proof state:
⊢ (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹

Tactic:
ext x : 1

Result:
case h
x : ℝ≥0
⊢ x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹

Proof state:
⊢ InvOn (fun x => 1 - (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}

Tactic:
have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ := by
  ext x : 1
  field_simp
  simp [tsub_mul, inv_mul_cancel₀]

Result:
this : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
⊢ InvOn (fun x => 1 - (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}

Proof state:
case left
this✝ : (fun x => x * (1 + x)⁻¹) = fun x => 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
this : 0 < 1 - x
⊢ (fun x => x * (1 + x)⁻¹) ((fun x => x * (1 - x)⁻¹) x) = x

Tactic:
field_simp [tsub_add_cancel_of_le hx.le, tsub_tsub_cancel_of_le hx.le]

Result:
no goals

Proof state:
case h
x : ℝ≥0
⊢ x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹

Tactic:
field_simp

Result:
case h
x : ℝ≥0
⊢ x = (1 - 1 / (1 + x)) * (1 + x)
-- Mathlib/Topology/Order.lean
theorem coinduced_sSup {s : Set (TopologicalSpace α)} :
    TopologicalSpace.coinduced f (sSup s) = sSup ((TopologicalSpace.coinduced f) '' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)

Tactic:
rw [sSup_eq_iSup', sSup_image', coinduced_iSup]

Result:
no goals
-- Mathlib/RepresentationTheory/Rep.lean
theorem linearization_single (X : Action (Type u) G) (g : G) (x : X.V) (r : k) :
    ((linearization k G).obj X).ρ g (Finsupp.single x r) = Finsupp.single (X.ρ g x) r

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) G
g : G
x : X.V
r : k
⊢ (((linearization k G).obj X).ρ g) (Finsupp.single x r) = Finsupp.single (X.ρ g x) r

Tactic:
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma IsAffineOpen.fromSpecStalk_closedPoint {U : Opens X} (hU : IsAffineOpen U)
    {x : X} (hxU : x ∈ U) :
    (hU.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (ConcreteCategory.hom (hU.fromSpecStalk hxU).base) (closedPoint ↑(X.presheaf.stalk x)) = x

Tactic:
rw [IsAffineOpen.fromSpecStalk, Scheme.comp_base_apply]

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (ConcreteCategory.hom hU.fromSpec.base)
      ((ConcreteCategory.hom (Spec.map (X.presheaf.germ U x hxU)).base) (closedPoint ↑(X.presheaf.stalk x))) =
    x

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (ConcreteCategory.hom hU.fromSpec.base)
      ((ConcreteCategory.hom (Spec.map (X.presheaf.germ U x hxU)).base) (closedPoint ↑(X.presheaf.stalk x))) =
    x

Tactic:
rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_min_distrib_left : ∀ (a b c : Nat), max a (min b c) = min (max a b) (max a c)
  | 0, _, _ => by simp only [Nat.zero_max]
  | _, 0, _ => by
    rw [Nat.zero_min, Nat.max_zero]
    exact Nat.min_eq_left (Nat.le_max_left ..) |>.symm
  | _, _, 0 => by
    rw [Nat.min_zero, Nat.max_zero]
    exact Nat.min_eq_right (Nat.le_max_left ..) |>.symm
  | _+1, _+1, _+1 => by
    simp only [Nat.succ_max_succ, Nat.succ_min_succ]
    exact congrArg succ <| Nat.max_min_distrib_left ..

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ max (n✝² + 1) (min (n✝¹ + 1) (n✝ + 1)) = min (max (n✝² + 1) (n✝¹ + 1)) (max (n✝² + 1) (n✝ + 1))

Tactic:
simp only [Nat.succ_max_succ, Nat.succ_min_succ]

Result:
n✝² n✝¹ n✝ : Nat
⊢ (max n✝² (min n✝¹ n✝)).succ = (min (max n✝² n✝¹) (max n✝² n✝)).succ

Proof state:
x✝¹ x✝ : Nat
⊢ max 0 (min x✝¹ x✝) = min (max 0 x✝¹) (max 0 x✝)

Tactic:
simp only [Nat.zero_max]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ x✝¹ = min x✝¹ (max x✝¹ x✝)

Tactic:
exact Nat.min_eq_left (Nat.le_max_left ..) |>.symm

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ max x✝¹ (min 0 x✝) = min (max x✝¹ 0) (max x✝¹ x✝)

Tactic:
rw [Nat.zero_min, Nat.max_zero]

Result:
x✝¹ x✝ : Nat
⊢ x✝¹ = min x✝¹ (max x✝¹ x✝)

Proof state:
x✝¹ x✝ : Nat
⊢ max x✝¹ (min x✝ 0) = min (max x✝¹ x✝) (max x✝¹ 0)

Tactic:
rw [Nat.min_zero, Nat.max_zero]

Result:
x✝¹ x✝ : Nat
⊢ x✝¹ = min (max x✝¹ x✝) x✝¹

Proof state:
x✝¹ x✝ : Nat
⊢ x✝¹ = min (max x✝¹ x✝) x✝¹

Tactic:
exact Nat.min_eq_right (Nat.le_max_left ..) |>.symm

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ (max n✝² (min n✝¹ n✝)).succ = (min (max n✝² n✝¹) (max n✝² n✝)).succ

Tactic:
exact congrArg succ <| Nat.max_min_distrib_left ..

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is one iff the characteristic is zero. -/
lemma expChar_one_iff_char_zero (p q : ℕ) [CharP R p] [ExpChar R q] : q = 1 ↔ p = 0

Proof state:
case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
q : ℕ
inst✝¹ : ExpChar R q
inst✝ : CharP R 0
⊢ q = 1

Tactic:
exact expChar_one_of_char_zero R q

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0

Tactic:
exact char_zero_of_expChar_one R p

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 ↔ p = 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0

case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Proof state:
case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
q : ℕ
inst✝¹ : ExpChar R q
inst✝ : CharP R 0
⊢ q = 1

Proof state:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0

Tactic:
rintro rfl

Result:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
lemma log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    log (x * y) = log x + log y ↔ arg x + arg y ∈ Set.Ioc (-π) π

Proof state:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg

Tactic:
simp_rw [add_re, add_im, log_re, log_im, norm_mul,
  Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]

Result:
no goals

Proof state:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Set.Ioc (-π) π

Tactic:
refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀

Result:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
-- Mathlib/RingTheory/OreLocalization/OreSet.lean
lemma nonempty_oreSet_iff {R : Type*} [Ring R] {S : Submonoid R} :
    Nonempty (OreSet S) ↔ (∀ (r₁ r₂ : R) (s : S), r₁ * s = r₂ * s → ∃ s' : S, s' * r₁ = s' * r₂) ∧
      (∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s)

Proof state:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ Nonempty (OreSet S) →
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ ((∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) →
    Nonempty (OreSet S)

Proof state:
case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)

Tactic:
exact ⟨H, r', s', h⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ Nonempty (OreSet S) →
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
exact fun ⟨_⟩ ↦ ⟨ore_right_cancel, fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
H' : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)

Tactic:
choose r' s' h using H'

Result:
case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)

Proof state:
case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ ((∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) →
    Nonempty (OreSet S)

Tactic:
intro ⟨H, H'⟩

Result:
case mpr
R : Type u_1
inst✝ : Ring R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
H' : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
theorem rhs_cast {aig1 aig2 : AIG α} (s : FullAdderInput aig1)
    (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).rhs = s.rhs.cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).rhs = s.rhs.cast hcast

Tactic:
simp [cast]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem map_monomial (n : σ →₀ ℕ) (a : R) : map σ f (monomial R n a) = monomial S n (f a)

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ (map σ f) ((monomial R n) a) = (monomial S n) (f a)

Tactic:
classical
ext m
simp [coeff_monomial, apply_ite f]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ (map σ f) ((monomial R n) a) = (monomial S n) (f a)

Tactic:
ext m

Result:
case h
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (coeff S m) ((map σ f) ((monomial R n) a)) = (coeff S m) ((monomial S n) (f a))

Proof state:
case h
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (coeff S m) ((map σ f) ((monomial R n) a)) = (coeff S m) ((monomial S n) (f a))

Tactic:
simp [coeff_monomial, apply_ite f]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.desc_comp {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V)
    (h : Y ⟶ V) : coprod.desc g h ≫ f = coprod.desc (g ≫ f) (h ≫ f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
⊢ desc g h ≫ f = desc (g ≫ f) (h ≫ f)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_diff_left : Ico a b \ {a} = Ioo a b :=
  ext fun x => by simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b

Tactic:
simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem norm_eq_one_iff (z : ℂ) : ‖z‖ = 1 ↔ ∃ θ : ℝ, exp (θ * I) = z

Proof state:
case refine_2.intro
θ : ℝ
⊢ ‖cexp (↑θ * I)‖ = 1

Tactic:
exact Complex.norm_exp_ofReal_mul_I θ

Result:
no goals

Proof state:
case refine_1
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = z

Tactic:
calc
  exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
  _ = z :=norm_mul_exp_arg_mul_I z

Result:
no goals

Proof state:
case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1

Tactic:
rintro ⟨θ, rfl⟩

Result:
case refine_2.intro
θ : ℝ
⊢ ‖cexp (↑θ * I)‖ = 1

Proof state:
z : ℂ
⊢ ‖z‖ = 1 ↔ ∃ θ, cexp (↑θ * I) = z

Tactic:
refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩

Result:
case refine_1
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = z

case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1

Proof state:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑‖z‖ * cexp (↑z.arg * I)

Tactic:
rw [hz, ofReal_one, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False

Proof state:
a : Bool
h : (!a) = a
⊢ False

Tactic:
by_cases a <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_sum [Semiring S] (n : ℕ) (f : ℕ → R → S[X]) :
    coeff (p.sum f) n = p.sum fun a b => coeff (f a b) n

Proof state:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.sum f).coeff n = { toFinsupp := toFinsupp✝ }.sum fun a b => (f a b).coeff n

Tactic:
simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ (p.sum f).coeff n = p.sum fun a b => (f a b).coeff n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.sum f).coeff n = { toFinsupp := toFinsupp✝ }.sum fun a b => (f a b).coeff n